proposition: Lemma swapVarInOrEq : forall (sw : Swapping vc) v, !LIn v (ALRange sw) -> no_repeats (ALRange sw) -> disjoint (ALDom sw) (ALRange sw) -> (LIn (swapVar sw v) (ALRange sw) [+] (swapVar sw v =v )).
proof: Proof. intros. destruct (in_deq _ (DeqVtype vc) v (ALDom sw));[left | right]. - apply swapVarIn; auto. - apply swapVarNoChange; cpx. Qed.
imports: Swap AssociationList Eqdep_dec