proposition: Lemma TM_eval_halts Σ n (M : TM Σ n) q t q' t' : TM.eval M q t q' t' -> halt M q' = true.
proof: Proof. induction 1; eauto. Qed.
imports: Undecidability(TM.TMEncoding TM.TMinL TM.Util.TM_facts) Undecidability.L(Computability.MuRec) Undecidability.Synthetic.Definitions