proposition: Lemma halt_rw: forall p, Halt p <-> exists b, Run p b.
proof: Proof. split; intros. - auto using halt_to_run. - destruct H. eauto using run_to_halt. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop