proposition: Lemma decider_not_run_false_to_run_true: forall p i, Decider p -> ~ Run (p i) false -> Run (p i) true.
proof: Proof. intros. assert (H := H i). rewrite halt_rw in *. destruct H as (b, H). destruct b; intuition. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop