proposition: Lemma genPatSwappingSpec3 : forall {G : CFGV} {vc : VarSym G} {lgs : list (bool * GSym G)} (pts : Mixture lgs) (lvAvoid : list (vType vc)), let lswap := genPatSwapping pts lvAvoid in lForall (fun x => disjoint (ALDom x) (ALRange x)) lswap.
proof: Proof. intros. apply disjointlforall. subst lswap. apply genPatSwappingSpec2. Qed.
imports: SubstAux AlphaEqProps