proposition: Lemma recognizes_negative_to_not_in: forall p L, Recognizes p L -> forall i, Negative (p i) -> ~ L i.
proof: Proof. intros. inversion_clear H0. - eauto using recognizes_run_false_to_not_in. - eauto using recognizes_loop_to_not_in. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop