proposition: Theorem dec_rec_co_rec: forall L, Decidable L <-> (Recognizable L /\ Recognizable (compl L)).
proof: Proof. split; intros. - split. + apply decidable_to_recognizable. assumption. + apply decidable_to_co_recognizable. assumption. - destruct H. apply recognizable_co_recognizable_to_decidable; auto. Qed.
imports: Turing Coq.Bool.Bool