PrintForm Definitions grammar 1 Sections AutomataTheory Doc

At: derive refl 1 1 1 1

1. V: Type
2. T: Type
3. G: Grammar(V;T)
4. l: (V+T)*

||nil||+1 > 0

By: RWH (LemmaC Thm* ||nil|| = 0) 0

Generated subgoals:

None


About:
addnilnatural_numberuniverselistunion