proposition: Lemma InputHandler_backup_no_msgs : forall i d u o d' l, InputHandler backup i d = (u, o, d', l) -> l = [].
proof: Proof. simpl. unfold BackupInputHandler. intros. monad_unfold. find_inversion. auto. Qed.
imports: Verdi(Verdi HandlerMonad)