proposition: Theorem inputs_ge_outputs : forall net tr, step_async_star (params := Counter_MultiParams) step_async_init net tr -> trace_outputs tr <= trace_inputs tr.
proof: Proof. intros. apply inputs_eq_outputs_plus_inc_plus_ack in H. lia. Qed.
imports: Verdi(Verdi HandlerMonad)