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* i,j:. i > j Prop

Def {i..j} == {k:| i k < j }

Thm* m,n:. {m..n} Type

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

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

Thm* ||nil||

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

Def AB == B < A

Thm* i,j:. ij Prop

Def A == A False

Thm* A:Prop. (A) Prop