At: lquo rel refl 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))
Refl(x,y:A*//(x R y);u,v.u (
x,y. z:A*. g(z@
x) 
g(z@y)) v)
By:
Unfold `refl` 0
THEN
Reduce 0
Generated subgoals:None
About:
