At:
no repeats reverse11
1.
T: Type
2.
L: T List
3.
u: T
4.
v: T List
5.
no_repeats(T;rev(v)) no_repeats(T;v) (u v) & l_disjoint(T;rev(v);nil) & no_repeats(T;rev(v)) & no_repeats(T;[u]) no_repeats(T;v) & (u v)
By:
Obvious
Generated subgoals: