proposition: Lemma step_1_snoc_inv : forall st st' tr t, step_1_star st st' (tr ++ [t]) -> exists st2, step_1_star st st2 tr /\ step_1 st2 st' [t].
proof: Proof. Proof using. intros. find_apply_lem_hyp refl_trans_1n_n1_trace. invc H. - destruct tr; discriminate. - invc H4. exists x'. find_apply_lem_hyp app_inj_tail. intuition. subst. + apply refl_trans_n1_1n_trace. auto. + subst. constructor. auto. Qed.
imports: Verdi(Verdi HandlerMonad)