Structural induction on generic list

Question

In preparation for an exam, I've come upon the following problem. Given the constructors :

[]: -> T LIST


[a]:T-> T LIST


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

And the functions :

size(l) : T LIST -> N (number of elements in l)

reverse(l): T LIST -> T LIST ( reverses the order ofthe elements in the list)


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


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


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

Prove by structural induction that :

max?(e, l) -> max?(e, unique(reverse(l))) || max?(e, repeated(reverse(l)))

I've managed to simplify this to :

max?(e, l) -> 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 -> 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 -> List
    append([], L) = L
    append([e], L) = cons(e, L)
    append(cons(e, L1), L2) = cons(e, append(L1, L2))