proposition: Lemma denote_continuation_prefix_independent (m : M _) : continuation_sub m -> forall s l1 l2, reify m (s, l1 ++ l2) = let res := reify m (s, l2) in match res with | None => None | Some res => Some (res.1, (res.2.1, l1 ++ res.2.2)) end.
proof: Proof. intros [ k Hk ]. subst m. elim: k => // [A a s l1 l2|A p k IH s l1 l2]. by rewrite !reifyret. rewrite /= !reifybind. rewrite denote_prefix_independent /=; [ | now exists p ]. destruct (reify (denote M _ p) (s, l2)) as [ (a, (s', l)) | ]. - by rewrite IH. - reflexivity. Qed.
imports: Eqdep JMeq List ssreflect mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) hierarchy monad_lib state_lib trace_lib monad_model