At: lquo rel symm 1 1
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. z:A*. g(z@
a) 
g(z@b)
9. z: A*
10. g(z@b)
g(z@a)
By: BackThru 8
Generated subgoals:None
About:
