proposition: Lemma change_bvars_range_spec : forall lva sub, let sub' := (change_bvars_range lva sub) in sub === sub' # disjoint (flat_map (tBndngVarsDeep vc) (ALRange sub')) lva.
proof: Proof. induction sub as [ |(v,t) sub Hind]; allsimpl; cpx. repnd. pose proof (tcase (@RenAlphaAvoid G vc)). pose proof (tcase (@RenAlphaAlpha G vc)). dands; cpx; repeat (disjoint_reasoning). unfold AlphaEqSubst. simpl. dands; cpx. Qed.
imports: SubstAuxAlphaEq AlphaRen Term