At: Rl iff Rg 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. L: LangOver(A)
7. l:A*. L(l) 
g(l)
8. x: A*
9. y: A*
10. L 
A*Prop
(z:A*. g(z @ x) g(z @ y)) (z:A*. g(z @ x) g(z @ y))
By:
Analyze 0
THEN
Analyze 0
THEN
Trivial
Generated subgoals:None
About:
