PrintForm Definitions myhill nerode Sections AutomataTheory Doc

At: lang rel tran 1 1 1
1. A: Type
2. L: A*Prop
3. a: A*
4. b: A*
5. c: A*
6. z:A*. L(z @ a) L(z @ b)
7. z:A*. L(z @ b) L(z @ c)
8. z: A*
9. L(z @ a)

L(z @ c)
By: RWW "6 7" 9
Generated subgoals:

None

About:
applyuniversefunctionlistpropall