proposition: Lemma SSubstRespectsAlpha2 : forall {gs : GSym G} (a b : Term gs) (sa sb: SSubstitution vc), a == b -> (tSSubst (tSSubst a sa) sb) == (tSSubst (tSSubst b sa) sb).
proof: Proof. introv Ha. apply SSubstRespectsAlpha1. apply SSubstRespectsAlpha1. trivial. Qed.
imports: SubstAuxAlphaEq AlphaRen Term