proposition: Lemma recognizes_run_false_to_not_in: forall p L i, Recognizes p L -> Run (p i) false -> ~ L i.
proof: Proof. intros. intros N. apply H in N. assert (Hx: true = false) by eauto using run_fun. inversion Hx. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop