proposition: Lemma step_Some_correct s s' k k' t l : step (s, k) (Some t) (s', k') -> reify (denote_continuation M k) (s, l) = reify (denote_continuation M k') (s', rcons l t).
proof: Proof. intro Hstep. remember (s, k) as sk eqn: Heq. remember (Some t) as o eqn: Heqo. remember (s', k') as sk' eqn: Heq'. revert s s' k k' l Heq Heq' Heqo. induction Hstep as [ s A a f | s A B p f g | s A p1 p2 k | s A p1 p2 k | s p k | s n p k | fuel s c p k Htrue | fuel s c p k Hfalse | s c p k | s f | s s' f | s t' f ]; intros s1 s2 k1 k2 l [= Hs1 Hk1] [= Hs2 Hk2] Heqo; try discriminate Heqo. subst s1 k1 s2 k2. injection Heqo; intro; subst t. by rewrite /= reifybind reifystmark. Qed.
imports: Eqdep JMeq List ssreflect mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) hierarchy monad_lib state_lib trace_lib monad_model