Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T,S:
. 1-1-Corresp(T;S)
1-1-Corresp(S;T)
Applied Tactic:
UnivCD THENW Auto
Generated subgoals:
1
. 1-1-Corresp(S;T)