proposition: Lemma step_star_stop_inv s A a l sk : step_star (s, stop A a) l sk -> l = [] /\ sk = (s, stop A a).
proof: Proof. intro Hss. inversion Hss. - split; reflexivity. - subst. match goal with H : step _ _ _ |- _ => inversion H end. - subst. match goal with H : step _ _ _ |- _ => inversion H end. Qed.
imports: Eqdep JMeq List ssreflect mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) hierarchy monad_lib state_lib trace_lib monad_model