proposition: Theorem SSubstNestAsApp: tSSubst (tSSubst a sa) sb == tSSubst a ((SubstSub sa sb)++sb).
proof: Proof. pose proof (change_bvars_rangewspec (rangeFreeVars sb) sa) as Hfs. exrepnd. rename sr into sa'. duplicate Hfs1 as Hb. apply SSubstRespectsAlpha with (a0:=a) (b:=a) in Hfs1; [|eauto with Alpha]. apply SSubstRespectsAlpha1 with (sa0:=sb) in Hfs1. eapply (tcase alphaEqTransitive); [apply Hfs1|]. assert (AlphaEqSubst (SubstSub sa sb ++ sb) (SubstSub sa' sb ++ sb)) as Hals by (apply AlphaEqSubstApp;[apply SSubstSubRespectsAlpha; assumption | eauto with Alpha]). apply SSubstRespectsAlpha with (a0:=a) (b:=a) in Hals; [|eauto with Alpha]. apply (tcase alphaEqSym) in Hals. eapply (tcase alphaEqTransitive); [| apply Hals]. 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. eapply (tcase alphaEqTransitive); [apply Hfr1 | ]. clear Hfr1. apply SSubstRespectsAlpha1 with (sa0:=(SubstSub sa sb ++ sb)) in Hfr2. apply (tcase alphaEqSym) in Hfr2. eapply (tcase alphaEqTransitive); [| apply Hfr2 ]. clear dependent a. unfold tSSubst. repeat (disjoint_reasoning). pattern (tRenAlpha ar (fvr sa)). rewrite <- (tcase RenAlphaNoChange) by cpx. rewrite <- (tcase RenAlphaNoChange) by (apply (tcase (@SSubstAuxBVarsDisjoint G vc)); cpx). rewrite <- (tcase RenAlphaNoChange); [ |rewrite rangeFreeVarsApp; disjoint_reasoning; cpx;[]; apply disjoint_sym; apply SubstSubFVarsDisjoint; repeat(disjoint_reasoning); fail]. rewrite SubstSubAsSubstAux; cpx;[]. apply talphaEqRefl. apply (tcase (@SSubstAuxNestAsApp G vc)). cpx. Qed.
imports: SubstAuxAlphaEq AlphaRen Term