proposition: Lemma invert_red_apply_cont: forall k c s c' s', red (apply_cont k c, s) (c', s') -> red_apply_cont_cases k c s c' s'.
proof: Proof. induction k; simpl; intros. - change c' with (apply_cont Kstop c'). apply racc_base; auto. - specialize (IHk _ _ _ _ H). inversion IHk; subst. + inversion H0; clear H0; subst. * apply racc_skip_seq. * change (apply_cont k (c4;;c)) with (apply_cont (Kseq c k) c4). apply racc_base; auto. - specialize (IHk _ _ _ _ H). inversion IHk; subst. inversion H0; clear H0; subst. * apply racc_skip_while. * change (apply_cont k (c4;;WHILE b c)) with (apply_cont (Kwhile b c k) c4). apply racc_base; auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences Simulation)