Thm* V,T:Type, g:Grammar(V;T). g.prod ((V+T List)(V+T)*)*
Thm* A:Type, B:(AType), p:a:AB(a). 1of(p) A
About:
V,T:Type, g:Grammar(V;T). g.prod 
((V+T List
)
(V+T)*)*A:Type, B:(A
Type), p:a:AB(a). 1of(p) A
