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