proposition: Lemma genPatSwappingSpec4 : forall {G : CFGV} {vc : VarSym G} {lgs : list (bool * GSym G)} (pts : Mixture lgs) (lvAvoid : list (vType vc)), let lswap := genPatSwapping pts lvAvoid in map (@ALDom _ _) lswap= map (lvKeep lvAvoid) (LLBinders vc pts).
proof: Proof. intros. subst lswap. unfold genPatSwapping. unfold vFreshDistRenLL. AddFDLLSpec. repnd. dands; auto. Qed.
imports: SubstAux AlphaEqProps