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