proposition: Lemma subSwapAlpha: forall (sw : Swapping vc) (sub : SSubstitution vc), disjoint (ALDom sub ++ rangeFreeVars sub) (ALDom sw ++ ALRange sw) -> AlphaEqSubst sub (swapSub sub sw).
proof: Proof. induction sub as [| (v,t) sub Hind]; cpx. introv Hdis. allsimpl. rewrite rangeFreeVars_cons in Hdis. repeat (disjoint_reasoning). allsimpl. constructor; [symmetry; apply swapVarNoChange; cpx|]. dands; cpx. - apply alphaEqSwapNonFree. apply leavesLVarUnchanged1; repeat (disjoint_reasoning). - apply Hind; repeat (disjoint_reasoning). Qed.
imports: Term AssociationList Swap AlphaEqProps SubstAux