proposition: Lemma swapVarInj: forall {G : CFGV} {vc : VarSym G} (sw : Swapping vc) (va vb : vType vc), swapVar sw va = swapVar sw vb -> va = vb.
proof: Proof. induction sw. - simpl. auto. - simpl. introv Heq. apply IHsw in Heq. destruct a. allsimpl. revert Heq. cases_ifd Hda; cases_ifd Hdb; subst; cpx; cases_ifd Hdc; try cases_ifd Hdd; intros; subst; cpx. Qed.
imports: Swap AssociationList Eqdep_dec