Thm* V,T:Type, G:Grammar(V;T). RegG(G) Prop reg_g_wf

Thm* V,T:Type, G:Grammar(V;T). ConFreeG(G) Prop con_free_g_wf

Thm* V1,V2,T:Type, G1:Grammar(V1;T), G2:Grammar(V2;T). G1 = G2 Prop g_eq_wf

Thm* G:Grammar(V;T), l,m,n:(V+T)*. (l m) (m n) (l n) derive_trans

Thm* G:Grammar(V;T), l:(V+T)*. l l derive_refl

Thm* V,T:Type, G:Grammar(V;T). (V+T)*(V+T)*Prop derive_wf

Thm* V,T:Type, G:Grammar(V;T). (V+T)*(V+T)*Prop directly_derive_wf

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

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