proposition: Lemma lBoundVarsmBndngVars : forall {G : CFGV} {vc : VarSym G} (mp : MixtureParam) (m : Mixture mp) (lll : list (list nat)), subset (flatten (lBoundVars vc lll m)) (mBndngVars vc m ).
proof: Proof. introv Hin. rw lin_flat_map in Hin. exrepnd. rw in_map_iff in Hin1. exrepnd. rewrite mBndngVarsAsNth. subst. apply lin_flat_map in Hin0. exrepnd. rename x0 into nn. apply lin_flat_map. exists nn. dands;spc. apply getBVarsNthRangeContra in Hin2. apply LInSeqIff; dands; omega. Qed.
imports: CFGV Omega Eqdep_dec