proposition: Lemma decides_not_in_to_run_false: forall p L i, Decides p L -> ~ L i -> Run (p i) false.
proof: Proof. intros. destruct H. assert (Ha: Halt (p i)) by auto using decider_to_halt. rewrite halt_rw in *. destruct Ha as (b, Ha). destruct b; auto. contradict H0. eapply recognizes_run_true_to_in; eauto. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop