At: lang auto wf 1 1 1 1 1 1 1 1 1 1 1 1
1. Alph: Type
2. L: LangOver(Alph)
3. EquivRel x,y:Alph*. x L-induced Equiv y
4. g: (x,y:Alph*//(x L-induced Equiv y))
5. a: Alph
6. s1: Alph*
7. s2: Alph*
8. z: Alph*
9. L(z @ [a] @ s1) 
L(z @ [a] @ s2)
L(z @ (a.s1)) L(z @ (a.s2))
By: Reduce 9
Generated subgoals:None
About:
