Thm* V,T:Type, g:Grammar(V;T). g.prod ((V+T List)(V+T)*)* g_prod_wf
Thm* T:Type, l:(T List). ||l|| length_p_wf
V,T:Type, g:Grammar(V;T). g.prod 
((V+T List
)
(V+T)*)* g_prod_wf
== {l:(T*)| ||l|| > 0 }
V,T:Type, g:Grammar(V;T). g.prod ((V+T List)(V+T)*)* g_prod_wf
T:Type, l:(T List). ||l|| 
length_p_wf