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