n:{1...}, E:(nnProp). (EquivRel x,y:n. x E y) & (x,y:n. Dec(x E y)) (m:(n+1). m ~ (i,j:n//(i E j)))

BackThru Thm* i:, E:({i...}Prop). E(i) (k:{i+1...}. E(k-1) E(k)) (k:{i...}. E(k))

1	E:(11Prop). (EquivRel x,y:1. x E y) & (x,y:1. Dec(x E y)) (m:(1+1). m ~ (i,j:1//(i E j)))
2	n:{1+1...}. (E:((n-1)(n-1)Prop). (EquivRel x,y:(n-1). x E y) & (x,y:(n-1). Dec(x E y)) (m:(n-1+1). m ~ (i,j:(n-1)//(i E j)))) (E:(nnProp). (EquivRel x,y:n. x E y) & (x,y:n. Dec(x E y)) (m:(n+1). m ~ (i,j:n//(i E j))))

About: