proposition: Lemma it_up_ren_ge n delta x: x >= n -> it n up_ren delta x = n + delta (x - n).
proof: Proof. intros; rewrite it_up_ren_spec; destruct dec2; intuition idtac; lia. Qed.
imports: List Arith Lia Morphisms Undecidability.HOU(calculus.terms)