proposition: Theorem kdiverges_diverges: forall s c, kdiverges s c -> diverges s c.
proof: Proof. intros. apply (simulation_infseq _ _ _ _ _ _ simulation_cont_red _ _ H). constructor; auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences Simulation)