fact: Definition ack_in_flight_to_primary (l : list packet) : nat := length (filterMap (fun p => if msg_eq_dec (pBody p) ack then if name_eq_dec (pDst p) primary then Some tt else None else None) l).
imports: Verdi(Verdi HandlerMonad)