Require Import Undecidability.Synthetic.Definitions Undecidability.Synthetic.ReducibilityFacts.

Require Import Undecidability.TM.TM.
Require Import Undecidability.SystemF.SysF.

Require Undecidability.SystemF.Reductions.HaltTM_1_to_SysF_TYP.
Require Undecidability.SystemF.Reductions.SysF_TYP_to_SysF_TC.

Theorem reduction : HaltTM 1 ⪯ SysF_TC.
Proof.
  apply (reduces_transitive HaltTM_1_to_SysF_TYP.reduction).
  exact SysF_TYP_to_SysF_TC.reduction.
Qed.