PrintForm Definitions automata 5 Sections AutomataTheory Doc

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

14. f: nAlph
5. g: Alphn
6. InvFuns(n; Alph; f; g)
7. EquivRel x,y:Alph*. x E y
8. 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
equalapplyuniversepropnatural_number