Thm* V,T:Type, g:Grammar(V;T). g.init V

Thm* V,T:Type, g:Grammar(V;T). g.prod ((V+T List)(V+T)*)*

Def Grammar(V;T) == ((V+T List)(V+T)*)*V

Thm* V,T:Type{i}. Grammar(V;T) Type{i'}

Def T List == {l:(T*)| ||l|| > 0 }

Thm* T:Type. (T List) Type

Thm* A:Type, B:(AType), p:a:AB(a). 2of(p) B(1of(p))

Thm* A:Type, B:(AType), p:a:AB(a). 1of(p) A

Def ||as|| == Case of as; nil 0 ; a.as' ||as'||+1 (recursive)

Thm* A:Type, l:A*. ||l||

Thm* ||nil||

Thm* i,j:. i > j Prop