proposition: Lemma undecidable_SOL_satis: undecidable SOL_satis.
proof: Proof. apply (undecidability_from_reducibility H10p_undec). apply H10p_to_SOL_satis. Qed.
imports: Undecidability.Synthetic.Definitions Undecidability.Synthetic.Undecidability Undecidability.SOL.SOL Undecidability.SOL.Reductions(H10p_to_SOL) Undecidability.H10(H10p_undec)