proposition: Lemma genPatSwappingSpec : forall {G : CFGV} {vc : VarSym G} {lgs : list (bool * GSym G)} (pts : Mixture lgs) (lvAvoid : list (vType vc)), let lswap := genPatSwapping pts lvAvoid in length lswap = length lgs # no_repeats (flat_map (@ALRange _ _) lswap) # disjoint (flat_map (@ALRange _ _) lswap) (lvAvoid++(mAllVars pts)).
proof: Proof. intros. subst lswap. unfold genPatSwapping. unfold vFreshDistRenLL. AddFDLLSpec. repnd. unfold LLBinders in FdSpec. apply (f_equal (@length _)) in FdSpec. autorewrite with fast in FdSpec. dands; cpx. Qed.
imports: SubstAux AlphaEqProps