Level: Lib Thy Top: 1
Hypotheses:None
Conclusion:
E:
1 
1 
EquivRel(1;x,y.x E y) 
(x,y:1. Dec(x E y)) 
(
m:(1 + 1). 1-1-Corresp(m;i,j:1//(i E j)))
Applied Tactic: (UnivCD THENM ExRepD ...a)
Generated subgoals:1. m:(1 + 1). 1-1-Corresp(m;i,j:1//(i E j))