Level: Lib Thy Top: 1
Hypotheses:

  1. A :

Conclusion:

1-1-Corresp(A;A)

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

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