At: quotient of nsubn 2 1 2 1 1 2 1 1 2 1 1 1 1 3 1 1 2 2 1 1 1 1 1 1 1 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: nnProp
4. a:n. a E a
5. Sym x,y:n. x E y & Trans x,y:n. x E y
6. x,y:n. Dec(x E y)
7. EquivRel x,y:(n-1). x E y
8. m: (n-1+1)
9. f: m(i,j:(n-1)//(i E j))
10. g: (i,j:(n-1)//(i E j))m
11. InvFuns(m; i,j:(n-1)//(i E j); f; g)
12. x:m. f(x) 
i,j:n//(i E j)
13. a:n. a E a
14. a,b:n. (a E b) (b E a)
15. a,b,c:n. (a E b) (b E c) (a E c)
16. x,y:i,j:n//(i E j). Dec(x = y)
17. Eb: (i,j:n//(i E j))(i,j:n//(i E j))
18. x,y:i,j:n//(i E j). (x Eb y) 
x = y
19. k: (n-1)
20. k E (n-1)
21. x1: n
22. x2: n
23. x1 E x2
24. n-1 i,j:n//(i E j)
25. x1 Eb (n-1)
26. 
(x2 Eb (n-1))
27. x2 = n-1 n
(n-1) E (n-1)
By: BackThru 4
Generated subgoals:None
About:
