proposition: Lemma swapLVar_subtractv : forall {G : CFGV} {vc : VarSym G} s l1 l2, @swapLVar G vc s (subtractv l1 l2) = subtractv (swapLVar s l1) (swapLVar s l2).
proof: Proof. introv. unfold swapLVar, subtractv. apply map_diff_commute; auto. Qed.
imports: Swap AssociationList Eqdep_dec