proposition: Lemma run_to_halt: forall p b, Run p b -> Halt p.
proof: Proof. intros. induction H. - constructor. - eapply halt_call; eauto. - eapply halt_seq; eauto. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop