Level: Lib Thy Top: 1
Hypotheses:None
Conclusion:
S,T:
.
(
n:
. f:n 
S. Bij(n;S;f)) 
(n:. f:n T. Bij(n;T;f))
(n:. f:n S T. Bij(n;S T;f))
Applied Tactic: RWH (LemmaC `bij_iff_1_1_corr`) 0
THENW Auto
Generated subgoals:1. S,T:. (n:. 1-1-Corresp(n;S)) (n:. 1-1-Corresp(n;T)) (n:. 1-1-Corresp(n;S T))