proposition: Theorem H10C_SAT_RA_UNIV_HALT : H10C_SAT ⪯ RA_UNIV_HALT.
proof: Proof. exists H10C_RA_UNIV; intros lc. unfold H10C_RA_UNIV. destruct (nat_h10lc_surj lc) as (k & Hk). symmetry; apply ra_univ_spec; auto. Qed.
imports: List Undecidability.MuRec.Util(recalg ra_univ ra_univ_andrej) Undecidability.MuRec.Util.RA_UNIV_HALT Undecidability.DiophantineConstraints.H10C Undecidability.Synthetic.Definitions