proposition: Lemma sdkfd: forall {G : CFGV} { vc : VarSym G} {ls : list (bool * (GSym G))} (llbn : list (list nat)) (lmix : Mixture ls) , lBoundVarsOld llbn lmix = lBoundVars vc llbn lmix .
proof: Proof. induction llbn; intros; allsimpl; cpx. f_equal. auto. Qed.
imports: CFGV Omega