Nuprl - Pf lang_auto

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))

< (s,a. a.s),nil,g > Automata(Alph;x,y:Alph*//(x L-induced Equiv y))

By: Unfold `automata` 0

Generated subgoals:

1 5. s: x,y:Alph*//(x L-induced Equiv y)
6. a: Alph
a.s x,y:Alph*//(x L-induced Equiv y)

2 nil x,y:Alph*//(x L-induced Equiv y)

About:

1	5. `s:` `x,y:Alph//(x L-induced Equiv y)` 6. `a:` `Alph` `a.s x,y:Alph//(x L-induced Equiv y)`
2	`nil x,y:Alph*//(x L-induced Equiv y)`