proposition: Lemma loop_to_not_halt: forall p, Loop p -> ~ Halt p.
proof: Proof. intros; induction H; intros N; inversion_clear N; try (contradict IHLoop; auto; fail). - apply H in H0. assumption. - contradict IHLoop. 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