proposition: Lemma SwapTermPatSpec : forall {G : CFGV} {vc : VarSym G}, (forall (s : GSym G) (ta : Term s), True) * (forall (s : GSym G) (pt : Pattern s) (swPat swTerm : Swapping vc) (lvA : list (vType vc)), subset (lvKeep lvA (pBndngVars vc pt)) (ALDom swPat) -> AvRenaming (lvA++ (pAllVars pt)) swPat -> AvRenaming (lvA++ (pAllVars pt)) swTerm -> disjoint (pAlreadyBndBinders vc pt) lvA -> disjoint lvA (pBndngVarsDeep vc (pSwapBindEmbed pt swPat swTerm))) * (forall (l : MixtureParam) (ma: Mixture l) (swPat swTerm : Swapping vc) (lvA : list (vType vc)), AvRenaming (lvA++ (mAllVars ma)) swTerm -> AvRenaming (lvA++ (mAllVars ma)) swPat -> disjoint (mAlreadyBndBinders vc ma) lvA -> subset (lvKeep lvA (mBndngVars vc ma)) (ALDom swPat) -> disjoint lvA (mBndngVarsDeep vc ( mSwapBindEmbed ma swPat swTerm)) ).
proof: Proof. intros. GInduction; cpx;[| | |]. - Case "pvleaf". introv Hsub H1a H2a Hd. clear H2a. repnud H1a. allsimpl. rewrite DeqSym. rewrite DeqSym in H1a. rewrite DeqSym in Hsub. ddeq; subst; allsimpl; cpx;[]. repeat(disjoint_reasoning). duplicate H1a as Hdis. eapply swapVarInOrEq in Hdis;cpx. dorn Hdis;[|]. + disjoint_lin_contra. + duplicate X. rw Hdis in X. rw memberb_din in Hsub. revert Hsub. cases_ifd Hs; introv Hsub;cpx. unfold subset in Hsub; allsimpl; dLin_hyp; try subst. eapply swapVarIn in H1a; cpx. disjoint_lin_contra. - Case "pembed". introv ? ? Hpa Hta. clear Hpa. allsimpl. repnud Hta. repeat(disjoint_reasoning). apply disjoint_sym. apply swapCommonBinders; cpx; [|repeat(disjoint_reasoning)];[]. unfold lvKeep. rewrite lKeepDisjoint; cpx. disjoint_reasoning. - Case "mtcons". introv. intros ? ? ? ?. introv H1a H2a Hd. allsimpl. repeat (disjoint_reasoning). repnud H2a. repnud H1a. apply H0; cpx; unfold AvRenaming; repeat(disjoint_reasoning). - Case "mpcons". introv. intros ? ? ? ?. introv H1a H2a Hd. allsimpl. repnud H2a. repnud H1a. repeat (disjoint_reasoning). + apply_hyp; cpx; unfold AvRenaming; dands;repeat(disjoint_reasoning);cpx. eapply subset_trans with (l2:=(lvKeep lvA (pBndngVars vc ph ++ mBndngVars vc ptl))); eauto. unfold lvKeep. apply monotoneFilter. eauto with SetReasoning. + apply_hyp; cpx; unfold AvRenaming; dands;repeat(disjoint_reasoning);cpx. eapply subset_trans with (l2:=(lvKeep lvA (pBndngVars vc ph ++ mBndngVars vc ptl))); eauto. unfold lvKeep. apply monotoneFilter. eauto with SetReasoning. Qed.
imports: SubstAux AlphaEqProps