proposition: Lemma it_up_var_sapp X A n delta e: (forall x, delta x >= x) -> n = length A -> subst_exp (A .+ var_exp) (ren_exp (it n up_ren delta) e) = subst_exp (A .+ delta >> @var_exp X) e.
proof: Proof. intros; subst. asimpl. eapply ext_exp. intros; unfold funcomp. assert (x < length A \/ x >= length A) as [] by lia. + rewrite it_up_ren_lt; eauto. eapply nth_error_lt_Some in H0 as [a]. erewrite !nth_error_sapp; eauto. + rewrite it_up_ren_ge; simplify; eauto. erewrite !sapp_ge_in; simplify; eauto. lia. Qed.
imports: List Arith Lia Morphisms Undecidability.HOU(calculus.terms)