Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
.
L:T List. ||L||
1
mem_f(T;hd(L);L)
Applied Tactic:
(D 0 THENM D 0 THENM ListInd 2 THENM Reduce 0 ...)
Generated subgoals:
1
. u = u
mem_f(T;u;v)
T:
. L:T List. ||L|| 
1 
mem_f(T;hd(L);L)
mem_f(T;u;v)