proposition: Lemma ndRenAlAxSpecDisjAux : forall {G : CFGV} {vc : VarSym G} {mp : MixtureParam} (pts : Mixture mp) (llbvOld llbvNew : list (lVars vc)) (lvA : list (vType vc)), disjoint (mAlreadyBndBinders vc pts) lvA -> lForall no_repeats llbvNew -> disjoint (flatten llbvNew) (lvA ++ mAllButBinders vc pts ++ flatten llbvOld) -> map (@length _) llbvOld = map (@length _) llbvNew -> length llbvOld = length mp -> disjoint (mAlreadyBndBinders vc pts ++ mBndngVars vc pts) lvA -> disjoint (mBndngVarsDeep vc (mLSwapTermEmbed pts llbvOld llbvNew)) lvA.
proof: Proof. induction pts; cpx;[|]. - introv H1a H2a H3a H4a H5a H6a. applydup map_eq_length_eq in H4a. allsimpl. dlist_len llbvOld. allsimpl. dlist_len llbvNew. allsimpl. inverts H4a. allrw no_repeats_app. repeat (disjoint_reasoning). + GC. apply tSwapBndngVarsDisjoint; cpx; repeat(disjoint_reasoning). + allsimpl. exrepnd. apply IHpts; cpx; repeat(disjoint_reasoning). - introv H1a H2a H3a H4a H5a H6a. applydup map_eq_length_eq in H4a. allsimpl. dlist_len llbvOld. allsimpl. dlist_len llbvNew. allsimpl. inverts H4a. allrw no_repeats_app. repeat (disjoint_reasoning). + GC. apply disjoint_sym. apply (pcase SwapEmbedSpec); cpx; autorewrite with fast; try congruence; cpx; repeat (disjoint_reasoning). + allsimpl. exrepnd. apply IHpts; cpx; repeat(disjoint_reasoning). Qed.
imports: AlphaEqProps Omega