At: Rl iff Rg 1 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. L: LangOver(A)
7. l:A*. L(l) 
g(l)
8. x: A*
9. y: A*
L 
A*Prop
By: Unfold `languages` 6
Generated subgoals:None
About:
