PrintForm Definitions myhill nerode Sections AutomataTheory Doc

At: lquo rel equi 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) & Sym u,v:x,y:A*//(x R y). u Rg v & Trans u,v:x,y:A*//(x R y). u Rg v
By: GenExRepD
Generated subgoals:

1 Refl(x,y:A*//(x R y);u,v.u Rg v)
2 Sym u,v:x,y:A*//(x R y). u Rg v
3 Trans u,v:x,y:A*//(x R y). u Rg v

About:
andquotientlistuniversefunction
propallimpliesbool