proposition: Lemma getBVarsNthRangeContra : forall {G : CFGV} {vc : VarSym G} (mp : MixtureParam) (m : Mixture mp) (nn: nat) (x : vType vc), LIn x (getBVarsNth vc m nn) -> nn < length mp.
proof: Proof. introv Hin. destruct (le_lt_dec (length mp) nn); cpx. rewrite getBVarsNthRange in Hin; cpx. Qed.
imports: CFGV Omega Eqdep_dec