proposition: Lemma SizePositive :forall {G : CFGV}, ( (forall (s : GSym G) (t : Term s), tSize t > 0 ) * (forall (s : GSym G) (pt : Pattern s), pSize pt > 0) * (forall (l : @MixtureParam G) (m : Mixture l), mSize m > 0)).
proof: Proof. intros. GInduction; intros; allsimpl; try omega. Qed.
imports: CFGV Omega