proposition: Lemma reject_recognize_to_accept_co_recognize: forall m1 m2 L, Recognizes m1 L -> Recognizes m2 (compl L) -> forall i, Run (m1 i) false -> Run (m2 i) true.
proof: Proof. eauto using recognizes_run_false_to_not_in, co_recognizes_not_in_to_run_true. Qed.
imports: Turing Coq.Bool.Bool