proposition: Lemma re_ren f delta: re f >> ren delta = re (f >> delta).
proof: Proof. fext; intros x; unfold funcomp, re. destruct tight; auto. now rewrite inhab_ren. Qed.
imports: List Arith Lia Morphisms Setoid Undecidability.HOU(calculus.calculus) Undecidability.HOU(unification.higher_order_unification unification.nth_order_unification concon.conservativity_constants concon.conservativity)