Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

T:. f:T . Fin(T) (fL:T List. t:T. (f t) mem_f(T;t;fL))

Applied Tactic: (RepD ...a)
Generated subgoals:

1. fL:T List. t:T. (f t) mem_f(T;t;fL)