proposition: Theorem eq_tm_not_decidable: ~ Decidable EQ_tm.
proof: Proof. intros N. apply dec_rec_co_rec in N. destruct N as (N, _). apply eq_tm_not_recognizable in N. assumption. Qed.
imports: Coq.Setoids.Setoid Turing.Turing Turing.LangDec Turing.LangRed