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