proposition: Lemma halt_seq_decider: forall p j (c:bool -> prog), Decider p -> (forall (b:bool), Run (p j) b -> Halt (c b)) -> Halt (Seq (p j) c).
proof: Proof. intros. apply halt_seq_alt. { apply H. } intros. apply H0. assumption. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop