proposition: Lemma ndRenAlAxSpecDisjAux : forall {G : CFGV} {vc : VarSym G} {mp : MixtureParam} (pts : Mixture mp) (lswPat lswTm : list (Swapping vc)) (lvA : list (vType vc)), disjoint (mAlreadyBndBinders vc pts) lvA -> lForall (AvRenaming (lvA++ (mAllVars pts))) lswTm -> lForall (AvRenaming (lvA++ (mAllVars pts))) lswPat -> length lswTm = length mp -> liftRelPtwise (fun _ _ _ => True) (fun s pt sw => subset (lvKeep lvA (pBndngVars vc pt)) (ALDom sw)) pts lswPat -> disjoint (mAlreadyBndBinders vc pts) lvA -> disjoint (mBndngVarsDeep vc (mSwapTermPat pts lswPat lswTm)) lvA.
proof: Proof. induction pts; cpx. - introv H1a H2a H3a H4a H5a H6a. allsimpl. destruct lswPat; cpx;[]. repnd. GC. destruct lswTm as [|swh swt]; inverts H4a. repeat (disjoint_reasoning). + GC. repnud H2a. repnud H2a0. apply swapCommonBinders; repeat (disjoint_reasoning); cpx. unfold lvKeep. rewrite lKeepDisjoint; cpx; disjoint_reasoning. + allsimpl. exrepnd. apply IHpts; cpx. * apply lForallSame. apply lForallSame in H2a. apply implies_lforall with (P:= (AvRenaming (lvA ++ tAllVars ph ++ mAllVars pts))); auto. introv xx. apply AvRenamingSubset; eauto. introv Hin. allrw in_app_iff. cpx. * apply lForallSame. apply lForallSame in H3a. apply implies_lforall with (P:= (AvRenaming (lvA ++ tAllVars ph ++ mAllVars pts))); auto. introv xx. apply AvRenamingSubset; eauto. introv Hin. allrw in_app_iff. cpx. - introv H1a H2a H3a H4a H5a H6a. allsimpl. destruct lswPat; cpx;[]. repnd. GC. destruct lswTm as [|swh swt]; inverts H4a. allsimpl. repnd. repeat (disjoint_reasoning);[|]. + GC. repnud H2a0. simpl. repnud H3a0. apply disjoint_sym. allsimpl. repnd. apply (pcase SwapTermPatSpec); repeat (disjoint_reasoning); cpx; unfold AvRenaming; cpx;dands; repeat (disjoint_reasoning); cpx. + allsimpl. exrepnd. apply IHpts; cpx. * apply lForallSame. apply lForallSame in H2a. apply implies_lforall with (P:= (AvRenaming (lvA ++ pAllVars ph ++ mAllVars pts))); auto. introv xx. apply AvRenamingSubset; eauto. introv Hin. allrw in_app_iff. cpx. * apply lForallSame. apply lForallSame in H3a. apply implies_lforall with (P:= (AvRenaming (lvA ++ pAllVars ph ++ mAllVars pts))); auto. introv xx. apply AvRenamingSubset; eauto. introv Hin. allrw in_app_iff. cpx. Qed.
imports: SubstAux AlphaEqProps