proposition: Lemma SubstAuxRespectsAlpha2 : forall (gs : GSym G) (ta tb : Term gs) (suba subb : SSubstitution vc), tAlphaEq vc ta tb -> AlphaEqSubst suba subb -> disjoint (tBndngVarsDeep vc ta) (rangeFreeVars suba) -> disjoint (tBndngVarsDeep vc tb) (rangeFreeVars subb) -> tAlphaEq vc (tSSubstAux ta suba) (tSSubstAux tb subb).
proof: Proof. introns Hyp. rewrite subAlphaSameFV with (subb:=subb) in Hyp1; eauto with Alpha;[]. duplicate Hyp. apply (ALtcase SubstAuxRespectsAlpha) with (sub:= subb) in Hyp; cpx; [|repeat (disjoint_reasoning); fail]. pose proof (tcase alphaEqAlphaSubst gs ta _ _ Hyp0). eauto with Alpha. Qed.
imports: Term AssociationList Swap AlphaEqProps SubstAux