proposition: Lemma co_recognizes_in_to_not_run_true: forall p L i, Recognizes p (compl L) -> L i -> ~ Run (p i) true.
proof: Proof. intros. intros N. apply H in N. contradiction. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop