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