Level: Lib Thy Top: 1
Hypotheses:

  1. T :

  2. f : T

  3. Fin(T)

Conclusion:

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

Applied Tactic: D (-1) THEN D (-1)
Generated subgoals:

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