Level: Lib Thy Top:
Hypotheses:None
Conclusion:
T:
. L,La:T List.
Fin(T)
(
La':T List
(t:T. mem_f(T;t;La) mem_f(T;t;L) 
mem_f(T;t;La'))
(t:T. mem_f(T;t;La') mem_f(T;t;La))
(||La'|| 
1 
mem_f(T;hd(La');L)))
Applied Tactic: (RepD THENM ListInd 3 THENM Reduce 0 ...)
Generated subgoals:1. La':T List
(t:T. False mem_f(T;t;L) mem_f(T;t;La'))
(t:T. mem_f(T;t;La') False)
(||La'|| 1 mem_f(T;hd(La');L))2. La':T List
(t:T. u = t mem_f(T;t;v) mem_f(T;t;L) mem_f(T;t;La'))
(t:T. mem_f(T;t;La') u = t mem_f(T;t;v))
(||La'|| 1 mem_f(T;hd(La');L))