PrintForm Definitions automata 5 Sections AutomataTheory Doc

At: fin alph list quo 1
1. Alph: Type
2. E: Alph*Alph*Prop
3. Fin(Alph) & (EquivRel x,y:Alph*. x E y) & (x,y:Alph*. Dec(x E y))

h:(Alph*Alph*). (x,y:Alph*. (x E y) h(x) = h(y)) & (x:Alph*. x E (h(x)))
By:
Analyze 3
THEN
Analyze 4
Generated subgoal:

13. Fin(Alph)
4. EquivRel x,y:Alph*. x E y
5. x,y:Alph*. Dec(x E y)
h:(Alph*Alph*). (x,y:Alph*. (x E y) h(x) = h(y)) & (x:Alph*. x E (h(x)))

About:
existsfunctionlistandall
equalapplyuniverseprop