proposition: Lemma apply_cont_is_skip: forall k c, apply_cont k c = SKIP -> k = Kstop /\ c = SKIP.
proof: Proof. induction k; cbn; intros. - auto. - apply IHk in H. intuition discriminate. - apply IHk in H. intuition discriminate. Qed.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences Simulation)