proposition: Theorem eq_tm_not_recognizable: ~ Recognizable EQ_tm.
proof: Proof. apply reducible_unrecognizable with (A:=compl A_tm); auto. - apply co_a_tm_red_eq_tm. - apply co_a_tm_not_recognizable. Qed.
imports: Coq.Setoids.Setoid Turing.Turing Turing.LangDec Turing.LangRed