proposition: Lemma decider_to_run: forall p i, Decider p -> exists b, Run (p i) b.
proof: Proof. intros. apply decider_to_halt with (i:=i) in H. rewrite halt_rw in *. assumption. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop