From Undecidability.H10 Require Import H10 H10_undec H10p Reductions.H10_to_H10p.
From Undecidability.Synthetic Require Import Undecidability.
Require Import Fin.
Local Set Implicit Arguments.
Theorem H10p_undec :
undecidable H10p.
Proof.
apply (undecidability_from_reducibility H10_undec). exact Reductions.H10_to_H10p.reduction.
Qed.
From Undecidability.Synthetic Require Import Undecidability.
Require Import Fin.
Local Set Implicit Arguments.
Theorem H10p_undec :
undecidable H10p.
Proof.
apply (undecidability_from_reducibility H10_undec). exact Reductions.H10_to_H10p.reduction.
Qed.