Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
A,B:
. 1-1-Corresp(A;B)
1-1-Corresp(B;A)
Applied Tactic:
(Unfold `one_one_corr` 0 THENM GenExRepD ...a)
Generated subgoals:
1
.
f:B
A.
g:A
B. InvFuns(B;A;f;g)
A,B:
. 1-1-Corresp(A;B) 
1-1-Corresp(B;A)
f:B 
A. g:A B. InvFuns(B;A;f;g)