proposition: Theorem a_tm_undecidable_alt: ~ Decidable A_tm.
proof: Proof. intros N. apply dec_rec_co_rec in N. destruct N as (_, N). apply co_a_tm_unrecognizable; auto. Qed.
imports: Coq.Setoids.Setoid Turing.Turing Turing.LangDec Turing.LangRed