PrintForm Definitions myhill nerode Sections AutomataTheory Doc

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

L(z @ b)
By: BackThru 5
Generated subgoals:

None

About:
applyuniversefunctionlistpropall