proposition: Lemma mBndngVarsSameIfNth : forall {G : CFGV} ( vc : VarSym G) {la : list (bool # GSym G)} (ma mb: Mixture la), (forall (nn : nat), getBVarsNth vc ma nn = getBVarsNth vc mb nn) -> mBndngVars vc ma = mBndngVars vc mb.
proof: Proof. intros. rewrite mBndngVarsAsNth. rewrite mBndngVarsAsNth. apply eq_flat_maps. intros nn Hinn. cpx. Qed.
imports: CFGV Omega Eqdep_dec