Structural induction over list

Question

I want to prove that unique(reverse(L)) = reverse(unique(L)) where L is a List.

List has the following constructors:
[] : -> List
[e] : Element -> List
cons(e, L) : Element x List -> List

I defined unique and reverse as follows:
unique : List -> List
reverse : List -> List

unique([]) = []
unique([e]) = [e]
unique(cons(e, L)) = cons(e, unique(L)), if member(e, L) = false unique(cons(e, L)) = unique(L), if member(e, L) = true

reverse([]) = []
reverse([e]) = [e]
reverse(cons(e, L)) = append(reverse(L), [e])

also,
member : Element x List -> {true, false}
member(e, []) = false
member(e, [a]) = (e == a) (true, if a is equal to e; false, if a isn't equal to e)
member(e, cons(a, L)) = (e == a) V member(e, L) (V is logical disjunction)

append : List x List -> List
append([], L) = L
append([e], L) = cons(e, L)
append(cons(e, L1), L2) = cons(e, append(L1, L2))

Both base cases are easy to verify.

Induction hypothesis: I assume unique(reverse(L)) = reverse(unique(L)) is true

Inductive step: I have to prove that unique(reverse(cons(e, L))) = reverse(unique(cons(e, L))) is true

I consider two cases:

1. member(e, L) = true, then:
   
   unique(reverse(cons(e, L))) = unique(append(reverse(L), [e]))

reverse(unique(cons(e, L))) = reverse(unique(L)) = unique(reverse(L))
   
   Those are obviously true, but I don't know how to formally prove it (I can explain it in words, but that's not the point).

2. member(e, L) = false, then:
   
   unique(reverse(cons(e, L))) = unique(append(reverse(L, [e])))

reverse(unique(cons(e, L))) = reverse(cons(e, unique(L))) = append(reverse(unique(L)), [e]) = append(unique(reverse(L)), [e])
   
   I'm stucked here.

unique, reverse, append and member don't have to be defined that way, but they have to do the same thing.