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