proposition: Lemma swapSubRevNoRep : forall (sw : Swapping vc) (sub: SSubstitution vc), no_repeats (ALDom sw) -> no_repeats (ALRange sw) -> disjoint (ALDom sw) (ALRange sw) -> swapSub sub sw = swapSub sub (rev sw).
proof: Proof. induction sub; cpx. intros. simpl. f_equal;cpx. f_equal. - apply swapVarRevNoRep; auto. - apply swapRevNoRep; auto. Qed.
imports: Term AssociationList Swap AlphaEqProps SubstAux