proposition: Lemma enc_ren n delta: ren delta (enc n) = enc n.
proof: Proof. unfold enc. cbn. do 2 f_equal. asimpl. now rewrite repeated_map. Qed.
imports: List Lia Undecidability.HOU(std.std calculus.calculus second_order.diophantine_equations) Undecidability.HOU.unification(systemunification nth_order_unification)