proposition: Theorem kterminates_terminates: forall s c s', kterminates s c s' -> terminates s c s'.
proof: Proof. intros. destruct (simulation_star _ _ _ _ _ _ simulation_cont_red _ _ H (c, s)) as ((c' & s'') & STAR & INV). constructor; auto. inversion INV; subst. apply STAR. Qed.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences Simulation)