PrintForm Definitions automata 5 Sections AutomataTheory Doc

At: fin alph list quo

Alph:Type, E:(Alph*Alph*Prop). 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: UnivCD
Generated subgoal:

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

About:
alluniversefunctionlistprop
impliesandexistsequalapply