proposition: Lemma SwapEmbedSpec : forall {G : CFGV} {vc : VarSym G}, (forall (s : GSym G) (ta : Term s), True) * (forall (s : GSym G) (pt : Pattern s) (sw: Swapping vc) (lvA : list (vType vc)), disjoint lvA (pBndngVars vc pt) -> disjoint (lvA++ (pAllButBinders vc pt) ++ (ALDom sw)) (ALRange sw) -> no_repeats (ALRange sw) -> disjoint (pAlreadyBndBinders vc pt) lvA -> disjoint lvA (pBndngVarsDeep vc (pSwapEmbed pt sw))) * (forall (l : MixtureParam) (ma: Mixture l) (sw : Swapping vc) (lvA : list (vType vc)), disjoint lvA (mBndngVars vc ma) -> disjoint (lvA++ (mAllButBinders vc ma) ++ (ALDom sw)) (ALRange sw) -> no_repeats (ALRange sw) -> disjoint (mAlreadyBndBinders vc ma) lvA -> disjoint lvA (mBndngVarsDeep vc (mSwapEmbed ma sw)) ).
proof: Proof. intros. GInduction; cpx;[| |]. - Case "pembed". introv ? ? Hpa Hta Hd. allsimpl. repeat(disjoint_reasoning). apply disjoint_sym. apply swapCommonBinders; cpx; [|repeat(disjoint_reasoning)];[]. unfold lvKeep. rewrite lKeepDisjoint; cpx. disjoint_reasoning. - Case "mtcons". introv. intros ? ? Hind ?. introv H1a H2a Hd. allsimpl. repeat (disjoint_reasoning). repnud H2a. repnud H1a. apply Hind; cpx;repeat(disjoint_reasoning). - Case "mpcons". introv. intros Hpind ? Hmind ?. introv H1a H2a Hd H2d. allsimpl. repeat(disjoint_reasoning);[|]. + apply Hpind; cpx; dands;repeat(disjoint_reasoning);cpx. + apply_hyp; cpx; dands;repeat(disjoint_reasoning);cpx. Qed.
imports: Swap AssociationList Eqdep_dec