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)))

nnProp

EquivRel x,y:n. x E y

x,y:n. Dec(x E y)

EquivRel x,y:(n-1). x E y

(n-1+1)

m(i,j:(n-1)//(i E j))

(i,j:(n-1)//(i E j))m

InvFuns(m; i,j:(n-1)//(i E j); f; g)

x:m. f(x) i,j:n//(i E j)

a:n. a E a

a,b:n. (a E b) (b E a)

a,b,c:n. (a E b) (b E c) (a E c)

x,y:i,j:n//(i E j). Dec(x = y)

(i,j:n//(i E j))(i,j:n//(i E j))

x,y:i,j:n//(i E j). (x Eb y) x = y

(k:(n-1). k E (n-1))

n-1 i,j:n//(i E j)

(m+1)(i,j:n//(i E j))

f1 = (x.if x=m n-1 else f(x) fi)

m:(n+1), f:(m(i,j:n//(i E j))), g:((i,j:n//(i E j))m). InvFuns(m; i,j:n//(i E j); f; g)

Let (g1 = (x.if x Eb (n-1) m else g(x) fi))

1	(x.if x Eb (n-1) m else g(x) fi) (i,j:n//(i E j))(m+1)
2	(i,j:n//(i E j))(m+1) Type{[1 | i 0]}
3	22. g1: (i,j:n//(i E j))(m+1) 23. g1 = (x.if x Eb (n-1) m else g(x) fi) m:(n+1), f:(m(i,j:n//(i E j))), g:((i,j:n//(i E j))m). InvFuns(m; i,j:n//(i E j); f; g)

About: