proposition: Proposition step_star_correct (s s' : S) (A : Type) (a : A) (p : program A) (l : list T) : step_star (s, p `; stop A) l (s', stop A a) -> reify (denote M _ p) (s, []) = Some (a, (s', l)).
proof: Proof. intro Hss. apply step_star_correct_gen with (l := []) in Hss. move: Hss. rewrite /= reifyret reifybind. destruct (reify (denote M _ p) (s, [])) as [[a'' [s'' l'']] | ]. - rewrite reifyret => -[Heq3 <- <-]. apply inj_pair2 in Heq3. by rewrite Heq3. - discriminate. Qed.
imports: Eqdep JMeq List ssreflect mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) hierarchy monad_lib state_lib trace_lib monad_model