PrintForm Definitions myhill nerode Sections AutomataTheory Doc

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

Sym u,v:x,y:A*//(x R y). u (x,y. z:A*. g(z@x) g(z@y)) v
By:
Unfold `sym` 0
THEN
Reduce 0
Generated subgoals:

16. a: x,y:A*//(x R y)
7. b: x,y:A*//(x R y)
8. z:A*. g(z@a) g(z@b)
9. z: A*
10. g(z@b)
g(z@a)
26. a: x,y:A*//(x R y)
7. b: x,y:A*//(x R y)
8. z:A*. g(z@a) g(z@b)
9. z: A*
10. g(z@a)
g(z@b)

About:
quotientlistlambdaallassertapply
universefunctionpropimpliesbool