At: mn 23 Rl equal Rg 1 1
1. Alph: Type
2. L: Alph*
Prop
3. R: Alph*Alph*Prop
4. EquivRel x,y:Alph*. x R y
5. 
x,y,z:Alph*. (x R y) 
((z @ x) R (z @ y))
6. g: (x,y:Alph*//(x R y))
7. l:Alph*. L(l) 
g(l)
8. x: Alph*
9. y: Alph*
L 
LangOver(Alph)
By: Unfold `languages` 0
Generated subgoals:None
About:
