proposition: Lemma SSubstSubRespectsAlpha : forall sa1 sb sa2, sa1 === sa2 -> SubstSub sa1 sb === SubstSub sa2 sb.
proof: Proof. intros ?. unfold AlphaEqSubst. induction sa1 as [|(v1,t1) subl1 Hind]; intros ? ? Hals; destruct sa2 as [|(v2,t2) subl2]; allsimpl;sp. unfold AlphaEqSubst. apply SSubstRespectsAlpha1; assumption. Qed.
imports: SubstAuxAlphaEq AlphaRen Term