PrintForm Definitions grammar 1 Sections AutomataTheory Doc

At: con free g wf 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

||[inl(a)]|| > 0
By: RWH (HypC 6) 0
Generated subgoal:

1 ||nil||+1 > 0

About:
consinlnilnatural_numberuniverseequalintadd