proposition: Lemma halt_to_run: forall p, Halt p -> exists b, Run p b.
proof: Proof. intros. induction H; try destruct IHHalt as (b, Hr). - exists b. constructor. - exists b. constructor. assumption. - destruct IHHalt as (b1, Hr). exists b1. econstructor; eauto. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop