At: mn 23 2 1 2 1 1 1 1 1 1 1 1 1
1. n: {1...}
2. A: Type
3. L: LangOver(A)
4. L 
A*
Prop
5. R: A*A*Prop
6. EquivRel x,y:A*. x R y
7. 
n ~ (x,y:A*//(x R y))
8. 
x,y,z:A*. (x R y) 
((z @ x) R (z @ y))
9. g: (x,y:A*//(x R y))
10. l:A*. L(l) 
g(l)
11. x,y:x,y:A*//(x R y). Dec(x Rg y)
12. EquivRel x,y:A*. x L-induced Equiv y
13. EquivRel u,v:x,y:A*//(x R y). u Rg v
14. x,y:A*//(x L-induced Equiv y) = x,y:A*//(x Rg y)
15. (x,y:A*//(x Rg y)) ~ (u,v:(x,y:A*//(x R y))//(u Rg v))
16. m: (n+1)
17. m ~ (u,v:(x,y:A*//(x R y))//(u Rg v))
18. (u,v:(x,y:A*//(x R y))//(u Rg v)) ~ (x,y:A*//(x Rg y))
19. m ~ (x,y:A*//(x Rg y))
m ~ (x,y:A*//(x L-induced Equiv y))
By: RevHypSubst 14 19
Generated subgoals:None
About:
