Require Import Undecidability.Synthetic.Undecidability.
Require Import FsubF_undec FsubD.
Require Import Reductions.FsubF_to_FsubD.
Lemma FsubD_SUBTYPE_undec : undecidable FsubD_SUBTYPE.
Proof.
apply (undecidability_from_reducibility FsubF_SUBTYPE_undec).
exact FsubF_to_FsubD.reduction.
Qed.