proposition: Theorem SysF_INH_undec : undecidable SysF_INH.
proof: Proof. apply (undecidability_from_reducibility H10C_SAT_undec). exact H10C_SAT_to_SysF_INH.reduction. Qed.
imports: Undecidability.Synthetic.Undecidability Undecidability.SystemF.SysF Undecidability.DiophantineConstraints.H10C_undec Undecidability.SemiUnification.SemiU_undec