proposition: Lemma Dowek X : H10 ⪯ SOU X 3.
proof: Proof. exists (H10_to_DWK X). intros E. split; eauto using H10_DWK, DWK_H10. Qed.
imports: List Arith Lia Undecidability.HOU(std.std calculus.calculus) Undecidability.HOU.second_order(diophantine_equations dowek.encoding) Undecidability.HOU.unification.nth_order_unification