At: shorten list 2 1 1 1
1. T: Type
2. L: T*
3. La: T*
4. Fin(T)
5. u: T
6. v: T*
7. La': T*
8. 
t:T. mem_f(T;t;v) 
mem_f(T;t;L) 
mem_f(T;t;La')
9. t:T. mem_f(T;t;La') mem_f(T;t;v)
10. ||La'||
1 
mem_f(T;hd(La');L)
11. mem_f(T;u;L)
12. t: T
13. u = t
mem_f(T;t;L) mem_f(T;t;La')
By:
RWH (HypC -1) -3
THEN
ProveProp
Generated subgoals:None
About:
