Structural induction on generic list In preparation for an exam, I've come upon the following problem.  Given the constructors :

[]: -&gt; T LIST


[a]:T-&gt; T LIST


cons(a,x) : T x T LIST -&gt; T LIST ( a is added to the beginning of the list)


And the functions : 

size(l) : T LIST -&gt; N (number of elements in l)

reverse(l): T LIST -&gt; T LIST ( reverses the order ofthe elements in the list)


unique(l) : T LIST -&gt; T LIST - returns a list of the elements in 'l' that only appear once


repeated(l) : T LIST -&gt; T LIST - returns a list of the elements in 'l' that appear more than once


max?(e,l) : T x T LIST -&gt; Bool - returns true if 'e' is the maximum element in the list, false otherwise


Prove by structural induction that :

max?(e, l) -&gt; max?(e, unique(reverse(l))) || max?(e, repeated(reverse(l)))


I've managed to simplify this to :

max?(e, l) -&gt; max?(e, unique(l)) || max?(e, repeated(l))


But I don't see how to proceed towards proving what is asked...

Used definitions of functions:

    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


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

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

    also,
    member : Element x List -&gt; Bool
    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 -&gt; List
    append([], L) = L
    append([e], L) = cons(e, L)
    append(cons(e, L1), L2) = cons(e, append(L1, L2))
Note: I mixed up boolean functions and propositions in what follows for 
brevity, and I hope it'll not cause any confusion.

I assume you have defined the function $\max?$ something like this:

max?(e, l) = ge_all?(e, l) &amp;&amp; member(e, l),


where

ge_all?(e, []) = True
ge_all?(e, cons(x,xs)) = e &gt;= x &amp;&amp; ge_all? e xs.


You will need a bunch of lemmas [they can be proved using structural induction]:

Lemma 1: $\text{member}(e, l) \implies \text{member}(e, \text{unique}(l)) \vee \text{member}(e, \text{repeated}(l))$ [this one is suggested by @Alexander]. Its proof is pretty boring because of lots of subcases.

Lemma 2: $\text{ge_all?}(e, l) \implies \text{ge_all?}(e, \text{unique}(l))$.

Lemma 3: $\text{ge_all?}(e, l) \implies \text{ge_all?}(e, \text{repeated}(l))$.

Theorem: $\max?(e,l) \implies \max?(e, \text{unique}(l)) \vee \max?(e, \text{repeated}(l))$.

Proof sketch:

$\max?(e, l)$ implies $\text{member}(e,l)$, which in its turn implies $\text{member}(e, \text{unique}(l)) \vee \text{member}(e, \text{repeated}(l))$ [by lemma 1]. So we consider two cases:
(1) $\text{member}(e,\text{unique}(l))$ and (2) $\text{member}(e,\text{repeated}(l))$.

In the case (1) we can prove $\text{max?}(e,\text{unique}(l))$ like this: $\max?(e, l)$ implies by definition $\text{ge_all?}(e,l)$, which [by lemma 2] implies $\text{ge_all?}(e,\text{unique}(l))$. Since $\text{ge_all?}(e,\text{unique}(l))$ and $\text{member}(e,\text{unique}(l))$ we get $\text{max?}(e,\text{unique}(l))$.

The case (2) is similar. End of proof.