proposition: Lemma it_up_ren_spec n delta x: it n up_ren delta x = if dec2 lt x n then x else n + delta (x - n).
proof: Proof. induction n in x, delta |-*; cbn. - destruct dec2; intuition idtac; rewrite ?Nat.sub_0_r; lia. - destruct x; cbn; destruct dec2; intuition idtac. lia. all: unfold funcomp; erewrite IHn. all: destruct dec2; intuition idtac; lia. Qed.
imports: List Arith Lia Morphisms Undecidability.HOU(calculus.terms)