Level: Lib Thy Top:
Hypotheses:None
Conclusion:
n:{1...}. 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: (BLemma `int_upper_ind` ...a)
Generated subgoals:1. 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)))2. 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))))