proposition: Lemma trace_well_formed : forall st st' trace, step_1_star st st' trace -> (trace = [] \/ exists t i o, trace = t ++ [(i, o)]).
proof: Proof. intros. find_apply_lem_hyp refl_trans_1n_n1_trace. invcs H; intuition. right. exists cs. invcs H1. unfold VarDHandler, VarDHandler' in *. vard_unfold. repeat break_match; simpl in *; repeat find_inversion; repeat eexists; eauto. Qed.
imports: Verdi(Verdi) Coq(FMapList String) Verdi(FMapVeryWeak StateMachineHandlerMonad)