proposition: Lemma getBVarsNthRange : forall {G : CFGV} {vc : VarSym G} (mp : MixtureParam) (m : Mixture mp) (nn: nat), nn >= length mp -> (getBVarsNth vc m nn) = [].
proof: Proof. induction m; introv Hgt; cpx; [Case "mtcons"|Case "mpcons"]; allsimpl. - simpl. allunfold ge. destruct nn; cpx. apply IHm. omega. - simpl. allunfold ge. destruct nn; cpx; try omega;[]. apply IHm. omega. Qed.
imports: CFGV Omega Eqdep_dec