proposition: Lemma inj_ren delta: inj >> ren delta = inj.
proof: Proof. fext; reflexivity. 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)