proposition: Lemma ndRenAlAxSpecDisj : forall {G : CFGV} {vc : VarSym G} {mp : MixtureParam} (pts : Mixture mp) (lln : list (list nat)) (lvAvoid : list (vType vc)), disjoint (mAlreadyBndBinders vc pts) lvAvoid -> disjoint (mBndngVarsDeep vc (nodeRenAlphaAux lln pts lvAvoid)) lvAvoid.
proof: Proof. introv Hdis. unfold nodeRenAlphaAux. remember (genPatSwapping pts lvAvoid) as ps. remember (genTermSwapping lln ps) as ts. pose proof (genPatSwappingSpec6 pts lvAvoid) as H6. allsimpl. exrepnd. apply ndRenAlAxSpecDisjAux; cpx. - admit. - subst ps; cpx. - admit. - apply genPatSwappingSpec5; cpx. subst ps; apply genPatSwappingSpec4; cpx. Qed.
imports: SubstAux AlphaEqProps