Level: Lib Thy Top: 1 1
Hypotheses:

  1. T :

  2. f : T

  3. n :

  4. f1 : n T

  5. Bij(n;T;f1)

Conclusion:

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

Applied Tactic: Assert k: k n (fL:T List (t:T. mem_f(T;t;fL) (f t)) (i:k. (f (f1 i)) mem_f(T;f1 i;fL)))
Generated subgoals:

1. k: k n (fL:T List. (t:T. mem_f(T;t;fL) (f t)) (i:k. (f (f1 i)) mem_f(T;f1 i;fL)))

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