proposition: Lemma genPatSwappingSpec2 : forall {G : CFGV} {vc : VarSym G} {lgs : list (bool * GSym G)} (pts : Mixture lgs) (lvAvoid : list (vType vc)), let lswap := genPatSwapping pts lvAvoid in disjoint (flat_map (@ALDom _ _) lswap) (flat_map (@ALRange _ _) lswap).
proof: Proof. intros. subst lswap. unfold genPatSwapping. unfold vFreshDistRenLL. AddFDLLSpec2. repnd; cpx. SetReasoning. apply subset_eq in FdSpec. eapply subset_trans; eauto. clear FdSpec FdSpec1 FdSpec2 FdSpec0 HeqFdLL FdLL. induction pts; allsimpl; cpx. - unfold LLBinders in IHpts. introv Hc. apply IHpts in Hc. allrw in_app_iff; cpx. - unfold LLBinders in IHpts. introv Hc. allrw in_app_iff. dorn Hc; cpx. + right. left. apply (pcase (bindersAllvarsSubset G vc)). unfold lvKeep in Hc. eauto 3 with SetReasoning. + apply IHpts in Hc. allrw in_app_iff; cpx. Qed.
imports: SubstAux AlphaEqProps