proposition: Lemma swapLVarDisjoint: forall (sw : Swapping vc) lv, disjoint lv (ALRange sw) -> no_repeats (ALRange sw) -> disjoint (ALDom sw) (ALRange sw) -> disjoint (swapLVar sw lv) (ALDom sw).
proof: Proof. induction lv; cpx. allsimpl. introv Hdis Hnt H2dis. apply disjoint_cons_l in Hdis. repnd. apply disjoint_cons_l. applydup IHlv in H2dis; cpx. dands; cpx. applydup swapVarInOrEq2 in Hdis; cpx;[]. repeat(in_reasoning); repnd; try subst; cpx. - introv Hin. disjoint_lin_contra. - rewrite Hdis2. sp. Qed.
imports: Swap AssociationList Eqdep_dec