proposition: Theorem SSubstNestSwap: disjoint (fvr sa) (Dom sb) -> disjoint (fvr sb) (Dom sa) -> disjoint (Dom sa) (Dom sb) -> tSSubst (tSSubst a sa) sb == tSSubst (tSSubst a sb) sa.
proof: Proof. introns Hdis. pose proof (change_bvars_rangewspec (rangeFreeVars sa) sb) as Hfs. exrepnd. rename sr into sb'. duplicate Hfs1 as Hdom. duplicate Hfs1 as Hfv. duplicate Hfs1 as Hb. unfold AlphaEqSubst in Hdom. apply ALRangeRelSameDom in Hdom. apply subAlphaSameFV in Hfv. apply SSubstRespectsAlpha with (a0:=a) (b:=a) in Hfs1; [|eauto with Alpha]. apply SSubstRespectsAlpha1 with (sa0:=sa) in Hfs1. eapply (tcase alphaEqTransitive); [ |apply (ALtcase alphaEqSym) ; apply Hfs1]. rewrite Hdom in Hdis. rewrite Hdom in Hdis1. rewrite Hfv in Hdis0. clear Hdom Hfv Hfs1. apply SSubstRespectsAlpha with (a0:=(tSSubst a sa)) (b:=(tSSubst a sa)) in Hb; [|eauto with Alpha]. eapply (tcase alphaEqTransitive); [apply Hb|]. clear dependent sb. rename sb' into sb. rename Hfs0 into Hdisrb. pose proof (change_bvars_rangewspec (rangeFreeVars sb) sa) as Hfs. exrepnd. rename sr into sa'. duplicate Hfs1 as Hdom. duplicate Hfs1 as Hfv. duplicate Hfs1 as Hb. unfold AlphaEqSubst in Hdom. apply ALRangeRelSameDom in Hdom. apply subAlphaSameFV in Hfv. apply SSubstRespectsAlpha with (a0:=a) (b:=a) in Hfs1; [|eauto with Alpha]. apply SSubstRespectsAlpha1 with (sa0:=sb) in Hfs1. eapply (tcase alphaEqTransitive); [ apply Hfs1 | ]. rewrite Hdom in Hdis1. rewrite Hdom in Hdis0. rewrite Hfv in Hdis. rewrite Hfv in Hdisrb. clear Hdom Hfv Hfs1. apply SSubstRespectsAlpha with (a0:=(tSSubst a sb)) (b:=(tSSubst a sb)) in Hb; [|eauto with Alpha]. apply (tcase alphaEqSym) in Hb. eapply (tcase alphaEqTransitive);[ | apply Hb]. clear dependent sa. rename sa' into sa. pose proof (tRenWithSpec a (fvr sa ++ fvr sb)) as Hfr. exrepnd. rename tar into ar. duplicate Hfr1. apply SSubstRespectsAlpha2 with (sa0:=sa) (sb0:=sb) in Hfr1. apply SSubstRespectsAlpha2 with (sa0:=sb) (sb0:=sa) in Hfr2. assert ((tSSubst (tSSubst ar sa) sb) == (tSSubst (tSSubst ar sb) sa)); [ | eauto with Alpha; fail]. clear dependent a. unfold tSSubst. repeat (disjoint_reasoning). pattern (tRenAlpha ar (fvr sa)). rewrite <- (tcase RenAlphaNoChange); sp;[]. pattern (tRenAlpha ar (fvr sb)). rewrite <- (tcase RenAlphaNoChange); sp;[]. rewrite <- (tcase RenAlphaNoChange); [| apply (tcase (@SSubstAuxBVarsDisjoint G vc)); cpx]. rewrite <- (tcase RenAlphaNoChange); [| apply (tcase (@SSubstAuxBVarsDisjoint G vc)); cpx]. apply talphaEqRefl. apply (tcase (@SSubstAuxNestSwap G vc)); repeat (disjoint_reasoning). Qed.
imports: SubstAuxAlphaEq AlphaRen Term