proposition: Lemma halt_seq_alt: forall p (c:bool -> prog), Halt p -> (forall (b:bool), Run p b -> Halt (c b)) -> Halt (Seq p c).
proof: Proof. intros. rewrite halt_rw in H. destruct H as (b, H). apply halt_seq with (b:=b); auto. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop