proposition: Lemma swapLVarNoChange : forall {G : CFGV} {vc : VarSym G} (sw : Swapping vc) (lv: list (vType vc)), disjoint lv (ALDom sw ++ ALRange sw) -> swapLVar sw lv = lv.
proof: Proof. induction lv; cpx. introns Hyp. allsimpl. repeat (disjoint_reasoning). f_equal;cpx. - apply swapVarNoChange; cpx. - apply IHlv. repeat (disjoint_reasoning). Qed.
imports: Swap AssociationList Eqdep_dec