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