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