PrintForm Definitions myhill nerode Sections AutomataTheory Doc

At: lquo rel equi 1 2
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))

Sym u,v:x,y:A*//(x R y). 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))). Sym u,v:x,y:A*//(x R y). u Rg v)
Generated subgoals:

None

About:
quotientlistuniversefunctionpropallimpliesbool