proposition: Lemma size_ren delta s: size (ren delta s) = size s.
proof: Proof. induction s in delta |-*; cbn; congruence. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)