NB: This requires bumping up the "depth" parameter of `rt_auto` and `rt_eauto`.

As a benefit, it becomes possible to automatically use RBFs in the
context of periodic tasks, sporadic tasks, and tasks with arrival
curves. Full example:

```
Require Import prosa.model.task.arrival.periodic.
Require Import prosa.model.task.arrival.periodic_as_sporadic.
Require Import prosa.model.task.arrival.sporadic_as_curve.
Require Import prosa.model.task.arrival.curve_as_rbf.

Section AutoArrivalModelConversion.

  Context {Job : JobType} `{JobArrival Job}.
  Context {Task : TaskType} `{PeriodicModel Task} `{JobTask Job Task}.

  Variable ts : TaskSet Task.

  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
  Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.

  Hypothesis H_valid_periods : valid_periods ts.
  Hypothesis H_respects : taskset_respects_periodic_task_model arr_seq ts.

  Context `{JobCost Job} `{TaskCost Task}.
  Hypothesis H_valid_costs : jobs_have_valid_job_costs.

  (** Interpret as an RBF. *)

  Goal valid_taskset_request_bound_function ts (task_max_rbf max_arrivals).
  Proof. by rt_auto. Qed.

  Goal taskset_respects_max_request_bound arr_seq ts.
  Proof. rt_eauto. Qed.

End AutoArrivalModelConversion.
```