PrintForm Definitions grammar 1 Sections AutomataTheory Doc

At: con free g wf

V,T:Type, G:Grammar(V;T). ConFreeG(G) Prop
By: Unfold `con_free_g` 0
Generated subgoal:

11. V: Type
2. T: Type
3. G: Grammar(V;T)
4. i: ||G.prod||
5. a: V
[inl(a)] (V+T List)

About:
alluniversememberpropunionconsinlnil