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