proposition: Lemma NetHandler_inc_in_flight_to_backup_preserved : forall p d u o d' l, NetHandler (pDst p) (pBody p) d = (u, o, d', l) -> d' + inc_in_flight_to_backup (send_packets (pDst p) l) = d + inc_in_flight_to_backup [p].
proof: Proof. unfold NetHandler, PrimaryNetHandler, BackupNetHandler. intros. monad_unfold. destruct p. simpl in *. repeat break_match; find_inversion; simpl; try rewrite inc_in_flight_to_backup_nil; unfold Data in *; compute; auto with *. Qed.
imports: Verdi(Verdi HandlerMonad)