Level: Lib Thy Top:
Hypotheses:None
Conclusion:
n:
. T:
. B:T 
. 1-1-Corresp(n;T) 
(t:T. Dec(B t)) 
(
m:. 1-1-Corresp(m;{t:T| B t} ))
Applied Tactic: (Unfold `one_one_corr` 0 THENM D 0 THENM NatInd 1 THENM GenRepD THENM ExRepD ...a)
Generated subgoals:1. m:. f:m {t:T| B t} . g:{t:T| B t} m. InvFuns(m;{t:T| B t} ;f;g)2. m:. f:m {t:T| B t} . g:{t:T| B t} m. InvFuns(m;{t:T| B t} ;f;g)