proposition: Lemma halt_to_not_loop: forall p, Halt p -> ~ Loop p.
proof: Proof. intros. induction H; intros N. - inversion_clear N. - inversion_clear N. contradict H. auto. - inversion_clear N. { apply loop_to_not_halt in H1. contradict H1. eapply run_to_halt; eauto. } assert (b0 = b) by eauto using run_fun. subst. contradiction. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop