proposition: Lemma input_handlers_InputHandlers : forall h i d os d' ms, input_handlers h i d = (os, d', ms) -> InputHandler h i d = (tt, os, d', ms).
proof: Proof. intros. simpl in *. monad_unfold. repeat break_let. find_inversion. destruct u. auto. Qed.
imports: Verdi(Verdi HandlerMonad)