proposition: Lemma swapLVarRevNoRep : forall {G : CFGV} {vc : VarSym G} (sw : Swapping vc) (sub: list (vType vc)), no_repeats (ALDom sw) -> no_repeats (ALRange sw) -> disjoint (ALDom sw) (ALRange sw) -> swapLVar sw sub = swapLVar (rev sw) sub.
proof: Proof. induction sub; cpx. intros. simpl. f_equal;cpx. apply swapVarRevNoRep; auto. Qed.
imports: Swap AssociationList Eqdep_dec