PrintForm Definitions myhill nerode Sections AutomataTheory Doc

At: lquo rel tran 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))

Trans u,v:x,y:A*//(x R y). u (x,y. z:A*. g(z@x) g(z@y)) v
By:
Unfold `trans` 0
THEN
Reduce 0
Generated subgoal:

1 a,b,c:x,y:A*//(x R y). (z:A*. g(z@a) g(z@b)) (z:A*. g(z@b) g(z@c)) (z:A*. g(z@a) g(z@c))

About:
quotientlistlambdaallassertapply
universefunctionpropimpliesbool