proposition: Lemma lBoundVarsLength : forall G {mp : MixtureParam} (vc : VarSym G) (m : Mixture mp) lln, length (lBoundVars vc lln m) = length lln.
proof: Proof. intros. unfold lBoundVars. autorewrite with fast. refl. Qed.
imports: CFGV Omega