proposition: Lemma injective_fun_swapVar : forall {G : CFGV} {vc : VarSym G} s, injective_fun (@swapVar G vc s).
proof: Proof. unfold swapVar, injective_fun. induction s; simpl; auto. introv k. apply IHs in k. destruct a. unfold oneSwapVar in k. ddeq; subst; sp. Qed.
imports: Swap AssociationList Eqdep_dec