Level: Lib Thy Top: 1
Hypotheses:

  1. T :

Conclusion:

(n:. f:n T. Bij(n;T;f)) (m:. 1-1-Corresp(m;T))

Applied Tactic: RWH (LemmaC `bij_iff_1_1_corr`) 0 THEN Auto
Generated subgoals:

None