proposition: Lemma diverges_equi: forall x y, x == y -> diverges x -> diverges y.
proof: Proof. cofix COINDHYP; intros. inversion H; subst. - elim (terminates_diverges_excl A x v); auto. - inversion H0; subst. constructor. eauto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP)