Structural induction over list
I am not entirely sure that what you're trying to prove is right.

unique [] = []
unique (x : xs) = if x `in` xs then unique xs else x : unique xs

reverse [] = []
reverse (x : xs) = reverse xs ++ [x]


If we take xs = [a, b, a, c] then:

unique [a, b, a, c]
= { unique.2 }
if a `in` [b, a, c] then unique [b, a, c] else a : unique [b, a, c]
= { ... }
[b, a, c]

reverse [b, a, c] = [c, a, b]

reverse [a, b, a, c] = [c, a, b, a]

unique [c, a, b, a]
= { unique.2 }
c : unique [a, b, a]
= { unique . 2 }
c : [b, a]
= [c, b, a]


Hence, unique (reverse [a, b, a, c]) = [c, b, a] and reverse (unique [a, b, a, c]) = [c, a, b].