proposition: Lemma swapLVar_app : forall {G : CFGV} {vc : VarSym G} s vs1 vs2, @swapLVar G vc s (vs1 ++ vs2) = swapLVar s vs1 ++ swapLVar s vs2.
proof: Proof. introv. unfold swapLVar. rw map_app; auto. Qed.
imports: Swap AssociationList Eqdep_dec