proposition: Lemma genPatSwappingSpec6 : 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 # lForall (AvRenaming (lvAvoid ++ mAllVars pts)) lswap.
proof: Proof. intros. subst lswap. pose proof (genPatSwappingSpec pts lvAvoid) as XX. pose proof (genPatSwappingSpec3 pts lvAvoid) as YY. allsimpl. remember (genPatSwapping pts lvAvoid) as pss. repnd. dands;cpx. repeat (disjoint_reasoning). clear XX0 Heqpss. induction pss; cpx. allsimpl. unfold AvRenaming. rw no_repeats_app in XX1. repnd. dands; repeat (disjoint_reasoning); cpx. Qed.
imports: SubstAux AlphaEqProps