proposition: Lemma getBVarsNth_swap : forall {G : CFGV} {vc : VarSym G} (p : MixtureParam) (m : Mixture p) x s, getBVarsNth vc (mSwap m s) x = swapLVar s (getBVarsNth vc m x).
proof: Proof. induction m; introv; simpl; auto; destruct x; simpl; auto. apply (snd (fst pBndngVars_swap)). Qed.
imports: Swap AssociationList Eqdep_dec