proposition: Lemma SSubstRespectsAlpha : a == b -> sa === sb -> tSSubst a sa == tSSubst b sb.
proof: Proof. introv Ha Has. unfold tSSubst. pose proof (ALtcase (@SubstAuxRespectsAlpha G vc)) as Hra. pose proof ((tcase (@RenAlphaAlpha G vc)) gs a (rangeFreeVars sa)) as Hala. pose proof ((tcase (@RenAlphaAlpha G vc)) gs b (rangeFreeVars sb)) as Halb. assert ((tRenAlpha a (rangeFreeVars sa)) == (tRenAlpha b (rangeFreeVars sb))) as Hx by eauto 4 with Alpha. pose proof (tcase (@RenAlphaAvoid G vc)) as Hav. apply SubstAuxRespectsAlpha2; cpx. Qed.
imports: SubstAuxAlphaEq AlphaRen Term