proposition: Theorem H10p_undec : undecidable H10p.
proof: Proof. apply (undecidability_from_reducibility H10_undec). exact Reductions.H10_to_H10p.reduction. Qed.
imports: Undecidability.H10(H10 H10_undec H10p Reductions.H10_to_H10p) Undecidability.Synthetic(Undecidability) Fin