Level: Lib Thy Top: 1 1
Hypotheses:

  1. T :

  2. t : T

  3. n :

  4. f : n T

  5. Bij(n;T;f)

Conclusion:

n > 0

Applied Tactic: Assert (n = 0)
Generated subgoals:

1. (n = 0)

2. n > 0