proposition: Lemma PB_input_handler_defn : forall h i d os d' ms, PB_input_handler h i d = (os, d', ms) -> (h = Primary /\ state d' = state d /\ os = [] /\ exists r, i = Request r /\ queue d' = queue d ++ [r] /\ (ms = [] \/ (ms = [(Backup, BackItUp r)] /\ queue d = []))) \/ (i = Read /\ d = d' /\ os = [ReadResponse (state d)] /\ ms = []) \/ (h = Backup /\ d = d' /\ ms = [] /\ os = []).
proof: Proof. Proof using. unfold PB_input_handler. intros. pb_unfold. repeat break_match; repeat find_inversion; intuition eauto. rewrite app_nil_r. simpl. find_apply_lem_hyp null_sound. find_rewrite. simpl. left. intuition. eexists. eauto. Qed.
imports: Verdi(Verdi HandlerMonad)