proposition: Lemma ndRenAlAxSpecDisj : forall {G : CFGV} {vc : VarSym G} {mp : MixtureParam} (pts : Mixture mp) (lln : list (list nat)) (lvAvoid : list (vType vc)), validBsl (length mp) lln -> length lln = length mp -> disjoint (mAlreadyBndBinders vc pts) lvAvoid -> disjoint (mBndngVarsDeep vc (nodeRenAlphaAux lln pts lvAvoid)) lvAvoid.
proof: Proof. introv Hnr Hlen Hdis. unfold nodeRenAlphaAux. cases_ifd Hdddd; cpx; [ apply disjointDeepShallowPlusAlready; repeat (disjoint_reasoning) |]. pose proof ((mcase (RenBindersSpec vc)) _ pts (lvAvoid ++ mAllVars pts)) as Hs. simpl in Hs. exrepnd. apply ndRenAlAxSpecDisjAux; try rewrite <- (mcase (RenBindersSpec2 vc)); try rewrite <- (mcase (RenBindersSpec3 vc)); cpx. - apply mRenBindersSpec3; cpx. - eapply subset_disjointLR; eauto. + apply lBoundVarsmBndngVars. + apply subset_app_lr; eauto;[]. apply subset_app. dands; eauto 2 with SetReasoning. - apply renBindersLBVLenSame. - unfold lBoundVars. autorewrite with fast. trivial. - repeat (disjoint_reasoning). Qed.
imports: AlphaEqProps Omega