PrintForm Definitions automata 5 Sections AutomataTheory Doc

At: fin alph list quo 1 1
1. Alph: Type
2. E: Alph*Alph*Prop
3. 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)))
By: Analyze 3
Generated subgoal:

13. n:
4. f:(nAlph). Bij(n; Alph; f)
5. EquivRel x,y:Alph*. x E y
6. 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