proposition: Lemma SubstAuxRespectsAlpha : ( (forall (gs : GSym G) (ta tb : Term gs), tAlphaEq vc ta tb -> forall (sub : SSubstitution vc), tAlphaEq vc ta tb -> disjoint (tBndngVarsDeep vc ta++tBndngVarsDeep vc tb) (rangeFreeVars sub) -> tAlphaEq vc (@tSSubstAux G vc gs ta sub) (tSSubstAux tb sub)) * (forall (gs : GSym G) (pa pb : Pattern gs), pAlphaEq vc pa pb -> forall (sub : SSubstitution vc), pAlphaEq vc pa pb -> disjoint (pBndngVarsDeep vc pa++pBndngVarsDeep vc pb) (rangeFreeVars sub) -> pAlphaEq vc (@pSSubstAux G vc gs pa sub) (pSSubstAux pb sub)) * (forall aa ab, AlphaEqAbs aa ab -> forall (sub : SSubstitution vc), AlphaEqAbs aa ab -> disjoint (abindersDeep aa++abindersDeep ab) (rangeFreeVars sub) -> AlphaEqAbs (aSSubstAux aa sub) (aSSubstAux ab sub)) * (forall la lb, lAlphaEqAbs la lb -> forall (sub : SSubstitution vc), lAlphaEqAbs la lb -> disjoint (albindersDeep la++albindersDeep lb) (rangeFreeVars sub) -> lAlphaEqAbs (alSSubstAux la sub) (alSSubstAux lb sub)) ).
proof: Proof. intros. GAlphaInd; introns Hyp; intros; allsimpl; cpx; eauto with Alpha; try constructor. - Case "tnode". allrw <- alSSubstAux_MakeAbstractionsTNode; auto. apply Hyp0; auto;repeat(disjoint_reasoning). + hide_hyp Hyp2. SetReasoning. unfold allBndngVars. eauto 3 with SetReasoning. + hide_hyp Hyp3. unfold allBndngVars. eauto 3 with SetReasoning. - Case "pembed". apply Hyp0; auto. - Case "pnode". allrw <- alSSubstAux_MakeAbstractionsPNode. apply Hyp0; auto; repeat(disjoint_reasoning); rewrite albndDeepMakeAbPSubset; auto. - Case "termAbs". rename Hyp5 into Htal. apply (betterAbsTElim (lbnew ++ lbva ++ (ALDom sub) ++ (rangeFreeVars sub) ++ (tBndngVarsDeep vc tma) ++ (tBndngVarsDeep vc tmb) ++ (tfreevars vc tma) ++ (tfreevars vc tmb) ++ tAllVars (tSSubstAux tma (ALFilter (DeqVtype vc) sub lbva)) ++ tAllVars (tSSubstAux tmb (ALFilter (DeqVtype vc) sub lbvb)) )) in Htal. allsimpl. exrepnd. rename lbnew0 into lbcnew. apply (tcase alphaEquiVariant ) in Htal0. specialize (Htal0 (combine lbcnew lbnew)). rewrite (tcase swap_app) in Htal0. rewrite (tcase swap_app) in Htal0. unfold tFresh in Htal3. unfold tFresh in Hyp1. allsimpl. repnd. match type of Htal0 with tAlphaEq _ _ ?r => remember r as ll end. autorewrite with slow in Htal0; try congruence; cpx; repeat (disjoint_reasoning). subst ll. autorewrite with slow in Htal0; try congruence; cpx; repeat (disjoint_reasoning). apply Hyp4 with (sub:= swapSub sub (combine lbnew lbcnew)) in Htal0. + apply alAbT with (lbnew:=lbcnew); try congruence; [unfolds_base; simpl; dands | | ]; cpx; repeat (disjoint_reasoning);[]. apply (tcase alphaEquiVariant ) in Htal0. specialize (Htal0 (combine lbnew lbcnew)). rewrite (tcase EquivariantSSubstAux) in Htal0. rewrite (tcase EquivariantSSubstAux) in Htal0. rewrite (tcase swap_app) in Htal0. rewrite (tcase swap_app) in Htal0. autorewrite with slow in Htal0; try congruence; cpx; repeat (disjoint_reasoning). rewrite swapSubRevNoRep in Htal0; auto; autorewrite with fast; cpx. autorewrite with SwapAppR in Htal0. autorewrite with fast in Htal0. rewrite (tcase EquivariantSSubstAux). rewrite (tcase EquivariantSSubstAux). rewrite (fun G S => tcase ( SSubstAuxSubFilter G S)) with (lf:= lbva) in Htal0 by (rewrite <- (tcase freevarsEquivariant); apply swapLVarDisjoint2; auto). remAlphaLeft Htal0 ll. rewrite (fun G S => tcase ( SSubstAuxSubFilter G S)) with (lf:= lbvb) in Htal0 by (rewrite <- (tcase freevarsEquivariant); apply swapLVarDisjoint2; auto). subst ll. dimp (subSwapAlpha (combine lbva lbcnew) (SubFilter sub lbva)); [ autorewrite with fast; try congruence; apply SubstFilterDisjAux; cpx; repeat(disjoint_reasoning)|]. dimp (subSwapAlpha (combine lbvb lbcnew) (SubFilter sub lbvb)); [ autorewrite with fast; try congruence; apply SubstFilterDisjAux; cpx; repeat(disjoint_reasoning)|]. remember (tSwap tma (combine lbva lbcnew)) as tmsa. remember (tSwap tmb (combine lbvb lbcnew)) as tmsb. remember (SubFilter sub lbva) as sfa. remember (SubFilter sub lbvb) as sfb. pose proof ((tcase alphaEqAlphaSubst) _ tmsa _ _ hyp). pose proof ((tcase alphaEqAlphaSubst) _ tmsb _ _ hyp0). repeat match goal with | [H : disjoint _ _ |- _] => clear H | [H : no_repeats _ |- _] => clear H | [H :_ = _ |- _] => clear H end. clear Hyp4 Hyp3 hyp hyp0. apply (tcase alphaEqSym) in X. eapply (tcase alphaEqTransitive). apply X. eapply (tcase alphaEqTransitive). apply Htal0. auto. + rewrite <- (tcase bndngVarsDeepEquivariant). rewrite <- (tcase bndngVarsDeepEquivariant). rewrite <- rangeFreeVarsEquivariant. eapply subset_disjoint_r with (l3 := (tBndngVarsDeep vc tmb)) in Hyp8; eauto 2 with SetReasoning;[]. eapply subset_disjoint_r with (l3 := (tBndngVarsDeep vc tma)) in Hyp7; eauto 2 with SetReasoning;[]. apply DisjointEquivariantRev with (sw:= (combine lbnew lbcnew)). match goal with [|- disjoint ?l _] => remember l as ld end. rewrite swapLVarRevNoRep; auto; autorewrite with fast; cpx. autorewrite with SwapAppR. autorewrite with fast. subst. rewrite swapLVar_app. rewrite swapLVarApp. rewrite swapLVarApp. autorewrite with slow; try congruence; cpx; repeat (disjoint_reasoning); apply disjointSwapLVar; autorewrite with fast; try congruence; repeat (disjoint_reasoning). - Case "patAbs". rename Hyp5 into Htal. apply (betterAbsPElim (lbnew ++ lbva ++ (ALDom sub) ++ (rangeFreeVars sub) ++ (pBndngVarsDeep vc tma) ++ (pBndngVarsDeep vc tmb) ++ (pfreevars vc tma) ++ (pfreevars vc tmb) ++ pAllVars (pSSubstAux tma (ALFilter (DeqVtype vc) sub lbva)) ++ pAllVars (pSSubstAux tmb (ALFilter (DeqVtype vc) sub lbvb)) )) in Htal. allsimpl. exrepnd. rename lbnew0 into lbcnew. apply (tcase alphaEquiVariant ) in Htal0. specialize (Htal0 (combine lbcnew lbnew)). rewrite (pcase swap_app) in Htal0. rewrite (pcase swap_app) in Htal0. unfold pFresh in Htal3. unfold pFresh in Hyp1. allsimpl. repnd. match type of Htal0 with pAlphaEq _ _ ?r => remember r as ll end. autorewrite with slow in Htal0; try congruence; cpx; repeat (disjoint_reasoning). subst ll. autorewrite with slow in Htal0; try congruence; cpx; repeat (disjoint_reasoning). apply Hyp4 with (sub:= swapSub sub (combine lbnew lbcnew)) in Htal0. + apply alAbP with (lbnew:=lbcnew); try congruence; [unfolds_base; simpl; dands | | ]; cpx; repeat (disjoint_reasoning);[]. apply (tcase alphaEquiVariant ) in Htal0. specialize (Htal0 (combine lbnew lbcnew)). rewrite (pcase EquivariantSSubstAux) in Htal0. rewrite (pcase EquivariantSSubstAux) in Htal0. rewrite (pcase swap_app) in Htal0. rewrite (pcase swap_app) in Htal0. autorewrite with slow in Htal0; try congruence; cpx; repeat (disjoint_reasoning). rewrite swapSubRevNoRep in Htal0; auto; autorewrite with fast; cpx. autorewrite with SwapAppR in Htal0. autorewrite with fast in Htal0. rewrite (pcase EquivariantSSubstAux). rewrite (pcase EquivariantSSubstAux). rewrite (fun G S => pcase ( SSubstAuxSubFilter G S)) with (lf:= lbva) in Htal0 by (rewrite <- (pcase freevarsEquivariant); apply swapLVarDisjoint2; auto). remAlphaLeft Htal0 ll. rewrite (fun G S => pcase ( SSubstAuxSubFilter G S)) with (lf:= lbvb) in Htal0 by (rewrite <- (pcase freevarsEquivariant); apply swapLVarDisjoint2; auto). subst ll. dimp (subSwapAlpha (combine lbva lbcnew) (SubFilter sub lbva)); [ autorewrite with fast; try congruence; apply SubstFilterDisjAux; cpx; repeat(disjoint_reasoning)|]. dimp (subSwapAlpha (combine lbvb lbcnew) (SubFilter sub lbvb)); [ autorewrite with fast; try congruence; apply SubstFilterDisjAux; cpx; repeat(disjoint_reasoning)|]. remember (pSwap tma (combine lbva lbcnew)) as tmsa. remember (pSwap tmb (combine lbvb lbcnew)) as tmsb. remember (SubFilter sub lbva) as sfa. remember (SubFilter sub lbvb) as sfb. pose proof ((pcase alphaEqAlphaSubst) _ tmsa _ _ hyp). pose proof ((pcase alphaEqAlphaSubst) _ tmsb _ _ hyp0). repeat match goal with | [H : disjoint _ _ |- _] => clear H | [H : no_repeats _ |- _] => clear H | [H :_ = _ |- _] => clear H end. clear Hyp4 Hyp3 hyp hyp0. apply (tcase alphaEqSym) in X. eapply (tcase alphaEqTransitive). apply X. eapply (tcase alphaEqTransitive). apply Htal0. auto. + rewrite <- (pcase bndngVarsDeepEquivariant). rewrite <- (pcase bndngVarsDeepEquivariant). rewrite <- rangeFreeVarsEquivariant. eapply subset_disjoint_r with (l3 := (pBndngVarsDeep vc tmb)) in Hyp8; eauto 2 with SetReasoning;[]. eapply subset_disjoint_r with (l3 := (pBndngVarsDeep vc tma)) in Hyp7; eauto 2 with SetReasoning;[]. apply DisjointEquivariantRev with (sw:= (combine lbnew lbcnew)). match goal with [|- disjoint ?l _] => remember l as ld end. rewrite swapLVarRevNoRep; auto; autorewrite with fast; cpx. autorewrite with SwapAppR. autorewrite with fast. subst. rewrite swapLVar_app. rewrite swapLVarApp. rewrite swapLVarApp. autorewrite with slow; try congruence; cpx; repeat (disjoint_reasoning); apply disjointSwapLVar; autorewrite with fast; try congruence; repeat (disjoint_reasoning). - apply Hyp0; repeat(disjoint_reasoning). - apply Hyp2; repeat(disjoint_reasoning). Qed.
imports: Term AssociationList Swap AlphaEqProps SubstAux