PrintForm Definitions myhill nerode Sections AutomataTheory Doc

At: mn 23 lem

Alph:Type, R:(Alph*Alph*Prop). Fin(Alph) (EquivRel x,y:Alph*. x R y) Fin(x,y:Alph*//(x R y)) (x,y,z:Alph*. (x R y) ((z @ x) R (z @ y))) (g:((x,y:Alph*//(x R y))), x,y:x,y:Alph*//(x R y). Dec(x Rg y))
By: RepeatFor 7 (Id THEN (Analyze 0))
Generated subgoal:

11. Alph: Type
2. R: Alph*Alph*Prop
3. Fin(Alph)
4. EquivRel x,y:Alph*. x R y
5. Fin(x,y:Alph*//(x R y))
6. x,y,z:Alph*. (x R y) ((z @ x) R (z @ y))
7. g: (x,y:Alph*//(x R y))
x,y:x,y:Alph*//(x R y). Dec(x Rg y)

About:
alluniversefunctionlistpropimpliesquotientbool