At: lang auto wf 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. s: x,y:Alph*//(x L-induced Equiv y)
6. a: Alph
a.s 
x,y:Alph*//(x L-induced Equiv y)
By: Unfold `member` 0
Generated subgoal:| 1 | a.s = a.s |
About:
