Require Import Undecidability.Synthetic.Definitions.

Require Import Undecidability.FRACTRAN.FRACTRAN.
From Undecidability.FRACTRAN.Deciders Require
  Halt_REV_FRACTRAN_dec.

Theorem Halt_REV_FRACTRAN_dec : decidable Halt_REV_FRACTRAN.
Proof.
  exists Halt_REV_FRACTRAN_dec.decide.
  exact Halt_REV_FRACTRAN_dec.decide_spec.
Qed.

Check Halt_REV_FRACTRAN_dec.