proposition: Lemma terminates_diverges_excl: forall (A: Type) (x: delay A) (v: A), terminates x v -> diverges x -> False.
proof: Proof. induction 1; intros D; inversion D; auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP)