proposition: Lemma decides_to_run: forall p L i, Decides p L -> exists b, Run (p i) b.
proof: Proof. intros. destruct H. specialize (H0 i). rewrite halt_rw in *. assumption. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop