Level: Lib Thy Top: 1
Hypotheses:

  1. T :

  2. P : T

  3. Q : T

  4. t:T. P t Q t

Conclusion:

1-1-Corresp({t:T| P t} ;{t:T| Q t} )

Applied Tactic: Unfold `one_one_corr` 0
Generated subgoals:

1. f:{t:T| P t} {t:T| Q t} . g:{t:T| Q t} {t:T| P t} . InvFuns({t:T| P t} ;{t:T| Q t} ;f;g)