PrintForm Definitions myhill nerode Sections AutomataTheory Doc

At: Rl iff Rg

A:Type, 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))), L:LangOver(A). (l:A*. L(l) g(l)) (x,y:A*. (x L-induced Equiv y) (x Rg y)))
By: UnivCD
Generated subgoals:

11. 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))
6. L: LangOver(A)
7. l:A*. L(l) g(l)
8. x: A*
9. y: A*
(x L-induced Equiv y) (x Rg y)
21. 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))
6. L: LangOver(A)
7. l: A*
L A*Prop

About:
alluniversefunctionlistpropimplies
quotientboolapplyassertmember