At: mn 23 2 1 1
1. n: {1...}
2. A: Type
3. L: LangOver(A)
4. L 
A*
Prop
5. R: A*A*Prop
6. Fin(A)
7. EquivRel x,y:A*. x R y
8. 
n ~ (x,y:A*//(x R y))
9. 
x,y,z:A*. (x R y) 
((z @ x) R (z @ y))
10. g: (x,y:A*//(x R y))
11. l:A*. L(l) 
g(l)
12. x: x,y:A*//(x R y)
13. y: x,y:A*//(x R y)
Dec(x Rg y)
By: BackThru
Thm* R:(Alph*Alph*Prop).
Fin(Alph)
(EquivRel x,y:Alph*. x R y)
Fin(x,y:Alph*//(x R y))
(x,y,z:Alph*. (x R y) ((z @ x) R (z @ y)))
(g:((x,y:Alph*//(x R y))), x,y:x,y:Alph*//(x R y). Dec(x Rg y))
Generated subgoal:| 1 | Fin(x,y:A*//(x R y)) |
About:
