proposition: Lemma SSubstRespectsAlpha1 : a == b -> (tSSubst a sa) == (tSSubst b sa).
proof: Proof. introv Ha. unfold tSSubst. pose proof ((tcase (@RenAlphaAlpha G vc)) gs a (rangeFreeVars sa)) as Hala. pose proof ((tcase (@RenAlphaAlpha G vc)) gs b (rangeFreeVars sa)) as Halb. pose proof (tcase (@RenAlphaAvoid G vc)) as Hav. apply (ALtcase (@SubstAuxRespectsAlpha G vc)); eauto with Alpha. repeat (disjoint_reasoning). Qed.
imports: SubstAuxAlphaEq AlphaRen Term