PrintForm Definitions grammar 1 Sections AutomataTheory Doc

At: con free g wf 1
1. V: Type
2. T: Type
3. G: Grammar(V;T)
4. i: ||G.prod||
5. a: V

[inl(a)] (V+T List)
By: Analyze
Generated subgoal:

1 ||[inl(a)]|| > 0

About:
memberunionconsinlniluniversenatural_number