proposition: Lemma step_1_star_singleton_trace : forall st st' i os, step_1_star st st' [(i, os)] -> step_1 st st' [(i, os)].
proof: Proof. Proof using. intros. invc H. invc H4. - rewrite app_nil_r in *. subst. auto. - invc H1. invc H. discriminate. Qed.
imports: Verdi(Verdi HandlerMonad)