2.
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)))3. E:
nnProp4. (EquivRel x,y:
n. x E y) & (x,y:n. Dec(x E y))
m:(n+1). m ~ (i,j:n//(i E j)) 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))))| 1 | 1. n: {1+1...} 2. 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)))3. E: nnProp4. (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:
 |  |  |  |  |
 |  |  |  |  |