PrintForm Definitions automata 4 Sections AutomataTheory Doc

At: lang auto wf 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. s: x,y:Alph*//(x L-induced Equiv y)
6. a: Alph

a.s = a.s
By: Analyze 5
Generated subgoal:

15. a: Alph
6. s1: Alph*
7. s2: Alph*
8. s1 L-induced Equiv s2
a.s1 = a.s2 x,y:Alph*//(x L-induced Equiv y)

About:
equalquotientlistconsuniversefunctionbool