proposition: Lemma trace_correct'_trace_correct : forall trace, trace_correct' init trace -> trace_correct trace.
proof: Proof. intros. remember init as x. induction H. - constructor. - subst. constructor; auto. find_rewrite_lem Map.empty_o. auto. Qed.
imports: Verdi(Verdi) Coq(FMapList String) Verdi(FMapVeryWeak StateMachineHandlerMonad)