proposition: Lemma MixMapLength : forall {T : Type} {G : CFGV} {lgs : MixtureParam} (ft: forall (gs : (GSym G)) (p : Term gs), T) (fp: forall (gs : (GSym G)) (p : Pattern gs), T) (pts : Mixture lgs), length (MixMap ft fp pts) = length lgs.
proof: Proof. induction pts; cpx. Qed.
imports: CFGV Omega