proposition: Lemma ren_plus_combine X n m s: @ren_exp X (plus n) (ren_exp (plus m) s) = ren_exp (plus (n + m)) s.
proof: Proof. rewrite ren_comp. f_equal. induction n; cbn; fext; intros; cbn. + reflexivity. + rewrite <-IHn. reflexivity. Qed.
imports: List Arith Lia Morphisms Undecidability.HOU(calculus.terms)