Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

A,B,C:. 1-1-Corresp(A;B) 1-1-Corresp(B;C) 1-1-Corresp(A;C)

Applied Tactic: (Unfold `one_one_corr` 0 THENM GenExRepD ...a)
Generated subgoals:

1. f:A C. g:C A. InvFuns(A;C;f;g)