proposition: Lemma trace_state_correct_trace_correct : forall st st' st'' trace t, trace_state_correct trace st st' -> trace_correct' st trace -> step_1 st' st'' t -> trace_correct' st (trace ++ t).
proof: Proof. intros. invcs H1; simpl in *. unfold VarDHandler, VarDHandler' in *. vard_unfold. repeat break_match; simpl in *; repeat find_inversion; constructor; auto; simpl in *; f_equal; eauto; break_if; simpl in *; f_equal; eauto; unfold trace_state_correct in *; exfalso; subst; repeat find_higher_order_rewrite; intuition. Qed.
imports: Verdi(Verdi) Coq(FMapList String) Verdi(FMapVeryWeak StateMachineHandlerMonad)