PrintForm Definitions myhill nerode Sections AutomataTheory Doc

At: mn quo append wf

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))) (z:A*, y:x,y:A*//(x R y). z@y x,y:A*//(x R y))
By: UnivCD
Generated subgoal:

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. z: A*
6. y: x,y:A*//(x R y)
z@y x,y:A*//(x R y)

About:
alluniversefunctionlistpropimpliesquotientmember