Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
. Fin(T)
(
TL:T List.
t:T. mem_f(T;t;TL))
Applied Tactic:
(RepD ...a)
Generated subgoals:
1
.
TL:T List.
t:T. mem_f(T;t;TL)
T:
. Fin(T) 
(
TL:T List. t:T. mem_f(T;t;TL))TL:T List. t:T. mem_f(T;t;TL)