proposition: Theorem output_eq_dec : forall x y: output, {x = y} + {x <> y}.
proof: Proof. decide equality; auto using key_eq_dec, value_eq_dec, val_eq_dec. Defined.
imports: Verdi(Verdi) Coq(FMapList String) Verdi(FMapVeryWeak StateMachineHandlerMonad)