proposition: Lemma enc_add n m: enc (n + m) ≡ add (enc n) (enc m).
proof: Proof. unfold add; rewrite enc_eta; asimpl. now rewrite enc_add'. Qed.
imports: List Lia Undecidability.HOU(std.std calculus.calculus second_order.diophantine_equations) Undecidability.HOU.unification(systemunification nth_order_unification)