PrintForm Definitions myhill nerode Sections AutomataTheory Doc

At: lquo rel equi 1 1
1. A: Type
2. R: A*A*Prop
3. EquivRel x,y:A*. x R y
4. x,y,z:A*. (x R y) ((z @ x) R (z @ y))
5. g: (x,y:A*//(x R y))

Refl(x,y:A*//(x R y);u,v.u Rg v)
By: BackThru Thm* R:(A*A*Prop). (EquivRel x,y:A*. x R y) (x,y,z:A*. (x R y) ((z @ x) R (z @ y))) (g:((x,y:A*//(x R y))). Refl(x,y:A*//(x R y);u,v.u Rg v))
Generated subgoals:

None

About:
quotientlistuniversefunctionpropallimpliesbool