proposition: Proposition step_star_complete (s s' : S) (A : Type) (a : A) (p : program A) (l : list T) : reify (denote M _ p) (s, []) = Some (a, (s', l)) -> step_star (s, p `; stop A) l (s', stop A a).
proof: Proof. intro Hp. apply step_star_complete_gen with (l1 := []). exact Hp. Qed.
imports: Eqdep JMeq List ssreflect mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) hierarchy monad_lib state_lib trace_lib monad_model