proposition: Lemma genPatSwappingSpec5 : forall {G : CFGV} {vc : VarSym G} {lgs : list (bool * GSym G)} (lvAvoid : list (vType vc)) (pts : Mixture lgs) (lswap : list (Swapping vc)), map (@ALDom _ _) lswap= map (lvKeep lvAvoid) (LLBinders vc pts) -> liftRelPtwise (fun _ _ _ => True) (fun s pt sw => subset (lvKeep lvAvoid (pBndngVars vc pt)) (ALDom sw)) pts lswap.
proof: Proof. unfold LLBinders. induction pts; introv Hmeq; destruct lswap as [| sh stl]; cpx. - allsimpl. dands; trivial. inverts Hmeq. rw H0 in H1. apply IHpts; cpx. - allsimpl. inverts Hmeq. dands; trivial; eauto. Qed.
imports: SubstAux AlphaEqProps