proposition: Lemma loop_alt_rw: forall p, Loop p <-> (forall b, ~ Run p b).
proof: Proof. split; intros. { rewrite loop_rw in H. intros N. contradict H. eauto using run_to_halt. } rewrite loop_rw. intros N. rewrite halt_rw in N. destruct N as (b, N). apply H in N. contradiction. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop