At: lquo rel tran 1 1 2
1. A: Type
2. R: A*
A*Prop
3. EquivRel x,y:A*. x R y
4. 
x,y,z:A*. (x R y) 
((z @ x) R (z @ y))
5. g: (x,y:A*//(x R y))
6. a: x,y:A*//(x R y)
7. b: x,y:A*//(x R y)
8. c: x,y:A*//(x R y)
9. z:A*. g(z@
a) 
g(z@b)
10. z:A*. g(z@b) g(z@c)
11. z: A*
12. g(z@c)
g(z@a)
By: RWW "9 < 10 < " 12
Generated subgoals:None
About:
