proposition: Lemma swapVarIn : forall (sw : Swapping vc) v, LIn v (ALDom sw) -> !LIn v (ALRange sw) -> no_repeats (ALRange sw) -> disjoint (ALDom sw) (ALRange sw) -> LIn (swapVar sw v) (ALRange sw).
proof: Proof. induction sw; simpl; introv i1 ni2 norep disj; auto; try (complete sp). allrw disjoint_cons_l; allrw disjoint_cons_r; repnd; allsimpl. allrw not_over_or; repnd. allrw no_repeats_cons; repnd. ddeq; try (complete sp);[]. rw swapVarNoChange; auto. Qed.
imports: Swap AssociationList Eqdep_dec