PrintForm Definitions grammar 1 Sections AutomataTheory Doc

At: con free g wf 1 1 1 1 1
1. V: Type
2. T: Type
3. G: Grammar(V;T)
4. i: ||G.prod||
5. a: V
6. ||[inl(a)]|| = ||nil||+1

||nil|| = 0
By: BackThru Thm* ||nil|| = 0
Generated subgoals:

None

About:
equalintnilnatural_numberuniverseconsinladd