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