Level: Lib Thy Top: 1
Hypotheses:

  1. T :

  2. t : T

  3. n :

  4. f : n T

  5. Bij(n;T;f)

Conclusion:

n:. f:n (T T). Bij(n;T T;f)

Applied Tactic: Assert n > 0
Generated subgoals:

1. n > 0

2. n:. f:n (T T). Bij(n;T T;f)