proposition: Theorem reduction : HaltTM 1 ⪯ SysF_TC.
proof: Proof. apply (reduces_transitive HaltTM_1_to_SysF_TYP.reduction). exact SysF_TYP_to_SysF_TC.reduction. Qed.
imports: Undecidability.Synthetic.Definitions Undecidability.Synthetic.ReducibilityFacts Undecidability.TM.TM Undecidability.SystemF.SysF