proposition: Theorem step_1_star_trace_correct : forall st trace, step_1_star init st trace -> trace_correct trace.
proof: Proof. intros. find_apply_lem_hyp step_1_star_trace_correct'. eauto using trace_correct'_trace_correct. Qed.
imports: Verdi(Verdi) Coq(FMapList String) Verdi(FMapVeryWeak StateMachineHandlerMonad)