proposition: Lemma inc_in_flight_to_backup_app : forall xs ys, inc_in_flight_to_backup (xs ++ ys) = inc_in_flight_to_backup xs + inc_in_flight_to_backup ys.
proof: Proof. intros. unfold inc_in_flight_to_backup. rewrite filterMap_app. rewrite app_length. auto. Qed.
imports: Verdi(Verdi HandlerMonad)