Level: Lib Thy Top: 1
Hypotheses:

  1. A :

  2. B :

  3. f : A B

  4. (f:A B. g:B A. InvFuns(A;B;f;g)) (n:. f:n B. Bij(n;B;f))

  5. Surj(A;B;f)

Conclusion:

Inj(A;B;f)

Applied Tactic: D 4 THEN D 4 THEN D 6 THEN D 5
Generated subgoals:

1. Inj(A;B;f)