proposition: Lemma recognizes_not_in_to_negative: forall p L, Recognizes p L -> forall i, ~ L i -> Negative (p i).
proof: Proof. intros. rewrite negative_rw. eauto using recognizes_not_in_to_not_run_true. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop