proposition: Lemma recognizes_not_in_to_not_run_true: forall p L, Recognizes p L -> forall i, ~ L i -> ~ Run (p i) true.
proof: Proof. intros. intros N. assert (L i). { eapply recognizes_run_true_to_in; eauto. } contradiction. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop