proposition: Lemma swapVarNoChange : forall v (sw : Swapping vc), !LIn v (ALDom sw) -> !LIn v (ALRange sw) -> swapVar sw v = v.
proof: Proof. induction sw; simpl; introv ni1 ni2; auto. allrw not_over_or; repnd. allsimpl. ddeq; try subst; sp. Qed.
imports: Swap AssociationList Eqdep_dec