proposition: Lemma PB_net_out_case : forall dst src m d os d' ms, PB_net dst src m d = (os, d', ms) -> (dst = Backup /\ os = [] /\ queue d' = queue d) \/ (dst = Primary /\ os = [] /\ d' = d) \/ (dst = Primary /\ exists h t, queue d = h :: t /\ queue d' = t /\ (let (us, st') := handler h (state d) in os = [RequestResponse h us] /\ state d' = st')).
proof: Proof. Proof using. intros. find_apply_lem_hyp PB_net_defn. intuition. - destruct dst; subst; intuition. - subst. right. right. intuition. break_exists. intuition eauto. Qed.
imports: Verdi(Verdi HandlerMonad)