proposition: Lemma halt_or_loop: forall p, Halt p \/ Loop p.
proof: Proof. induction p; intros. - destruct IHp as [IH|IH]. + apply halt_to_run in IH. destruct IH as (b, IH). assert (H := H b). destruct H as [H|H]. { left. econstructor; eauto. } right. eapply loop_seq_r; eauto. + right. eauto using loop_seq_l. - destruct (exec_exists m i) as [(b, He)|Hl]. { left. econstructor. eauto. } right. constructor. auto. - left. constructor. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop