PrintForm Definitions grammar 1 Sections AutomataTheory Doc

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

||[inl(a)]|| > 0
By: Inst Thm* a:A, as:A*. ||a.as|| = ||as||+1 [V+T;inl(a);nil]
Generated subgoal:

16. ||[inl(a)]|| = ||nil||+1
||[inl(a)]|| > 0

About:
consinlnilnatural_numberunionuniverse