proposition: Lemma swapVarImplies : forall (sw : Swapping vc) v w, w = swapVar sw v -> w = v [+] LIn w (ALDom sw) [+] LIn w (ALRange sw).
proof: Proof. simpl; induction sw as [| s sw IHvs1]; introv Heq; cpx. destruct s as [va vb]. allsimpl. apply IHvs1 in Heq. ddeq; sp; try subst; cpx. Qed.
imports: Swap AssociationList Eqdep_dec