proposition: Corollary reducible_unrecognizable: forall A B, A <=m B -> ~ Recognizable A -> ~ Recognizable B.
proof: Proof. intros A B Hred Ha Hb. contradict Ha. eauto using reducible_recognizable. Qed.
imports: Coq.Setoids.Setoid Turing.Turing