proposition: Lemma inputs_with_key_plus_key : forall l k i o, input_key i = k -> inputs_with_key (l ++ [(i, o)]) k = (inputs_with_key l k) ++ [i].
proof: Proof. induction l; intros; simpl in *. - unfold inputs_with_key. simpl in *. repeat break_match; congruence. - unfold inputs_with_key in *. simpl in *. repeat break_match; simpl in *; f_equal; eauto. Qed.
imports: Verdi(Verdi) Coq(FMapList String) Verdi(FMapVeryWeak StateMachineHandlerMonad)