proposition: Theorem step_1_star_trace_correct' : forall st st' trace, step_1_star st st' trace -> trace_correct' st trace.
proof: Proof. intros. find_apply_lem_hyp refl_trans_1n_n1_trace. induction H. - constructor. - find_apply_lem_hyp refl_trans_n1_1n_trace. find_apply_lem_hyp step_1_star_trace_state_correct; auto. eapply trace_state_correct_trace_correct; eauto. Qed.
imports: Verdi(Verdi) Coq(FMapList String) Verdi(FMapVeryWeak StateMachineHandlerMonad)