proposition: Lemma inputs_with_key_plus_not_key : forall l k i o, input_key i <> k -> inputs_with_key (l ++ [(i, o)]) k = (inputs_with_key l k).
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 *; eauto; try discriminate. repeat find_inversion. f_equal. eauto. Qed.
imports: Verdi(Verdi) Coq(FMapList String) Verdi(FMapVeryWeak StateMachineHandlerMonad)