Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
A,B:
.
f:A
B. 1-1-Corresp(A;B)
Fin(B)
Surj(A;B;f)
Inj(A;B;f)
Applied Tactic:
Unfold `one_one_corr` 0 THEN Unfold `finite` 0 THEN UnivCD THENA Auto
Generated subgoals:
1
. Inj(A;B;f)
A,B:
. f:A 
B. 1-1-Corresp(A;B) 
Fin(B) 
Surj(A;B;f) Inj(A;B;f)