proposition: Lemma co_recognizes_run_true_to_not_in: forall p L i, Recognizes p (compl L) -> Run (p i) true -> ~ L i.
proof: Proof. intros. apply recognizes_run_true_to_in with (L:=compl L) in H0; auto. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop