proposition: Lemma SubstSubAsSubstAux: forall (sa sb : SSubstitution vc), disjoint (flat_map (tBndngVarsDeep vc) (ALRange sa)) (fvr sb) -> SubstSub sa sb = tSSubstAux_sub sa sb.
proof: Proof. induction sa as [| (v,t) sa Hind]; introv Hd; allsimpl; [unfold rangeFreeVars; cpx |]. repeat (disjoint_reasoning). f_equal; cpx;[]. f_equal; cpx. unfold tSSubst. rewrite <- (tcase RenAlphaNoChange) by cpx. refl. Qed.
imports: SubstAuxAlphaEq AlphaRen Term