proposition: Lemma swapLVar_flat_map : forall {G : CFGV} {vc : VarSym G} A s f (l : list A), @swapLVar G vc s (flat_map f l) = flat_map (compose (swapLVar s) f) l.
proof: Proof. unfold swapLVar. introv. rw map_flat_map; sp. Qed.
imports: Swap AssociationList Eqdep_dec