proposition: Lemma swapCommonBinders : forall {G : CFGV} {vc : VarSym G}, (forall (s : GSym G) (ta : Term s) (sw: Swapping vc) (lvA : list (vType vc)), subset (lvKeep lvA (tBndngVarsDeep vc ta)) (ALDom sw) -> disjoint (ALRange sw) (lvA++ (tAllVars ta)) -> no_repeats (ALRange sw) -> disjoint (ALDom sw) (ALRange sw) -> disjoint (tBndngVarsDeep vc (tSwap ta sw)) lvA) * (forall (s : GSym G) (pt : Pattern s) (sw: Swapping vc) (lvA : list (vType vc)), subset (lvKeep lvA (pBndngVarsDeep vc pt)) (ALDom sw) -> disjoint (ALRange sw) (lvA++ (pAllVars pt)) -> no_repeats (ALRange sw) -> disjoint (ALDom sw) (ALRange sw) -> disjoint (pBndngVarsDeep vc (pSwap pt sw)) lvA) * (forall (l : MixtureParam) (ma: Mixture l) (sw: Swapping vc) (lvA : list (vType vc)), subset (lvKeep lvA (mBndngVarsDeep vc ma)) (ALDom sw) -> disjoint (ALRange sw) (lvA++ (mAllVars ma)) -> no_repeats (ALRange sw) -> disjoint (ALDom sw) (ALRange sw) -> disjoint (mBndngVarsDeep vc (mSwap ma sw)) lvA).
proof: Proof. introv. GInduction; cpx; eauto with slow;[| |]. - Case "pvleaf". introv Hsub Hdis Hsdid Hnr. allsimpl. rewrite DeqSym. rewrite DeqSym in Hdis. rewrite DeqSym in Hsub. ddeq; subst; allsimpl; cpx;[]. repeat(disjoint_reasoning). duplicate 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 Hdis1; cpx. disjoint_lin_contra. - Case "mtcons". introns Hyp. allsimpl. repeat (disjoint_reasoning). allrw in_app_iff. dorn Hyp5. + eapply Hyp in Hyp5; eauto; repeat(disjoint_reasoning). unfold lvKeep in Hyp1. unfold lKeep in Hyp1. rw filter_app in Hyp1. rw subset_app in Hyp1. repnd. cpx. + eapply Hyp0 in Hyp5; eauto; repeat(disjoint_reasoning). unfold lvKeep in Hyp1. unfold lKeep in Hyp1. rw filter_app in Hyp1. rw subset_app in Hyp1. repnd. cpx. - Case "mpcons". introns Hyp. allsimpl. repeat (disjoint_reasoning). allrw in_app_iff. dorn Hyp5. + eapply Hyp in Hyp5; eauto; repeat(disjoint_reasoning). unfold lvKeep in Hyp1. unfold lKeep in Hyp1. rw filter_app in Hyp1. rw subset_app in Hyp1. repnd. cpx. + eapply Hyp0 in Hyp5; eauto; repeat(disjoint_reasoning). unfold lvKeep in Hyp1. unfold lKeep in Hyp1. rw filter_app in Hyp1. rw subset_app in Hyp1. repnd. cpx. Qed.
imports: Swap AssociationList Eqdep_dec