proposition: Lemma InputHandler_trace_preserved : forall h i d u o d' l, InputHandler h i d = (u, o, d', l) -> trace_inputs [(h, inl i)] = trace_outputs [(h, inr o)] + inc_in_flight_to_backup (send_packets h l) + ack_in_flight_to_primary (send_packets h l).
proof: Proof. unfold InputHandler, PrimaryInputHandler, BackupInputHandler. simpl. intros. monad_unfold. repeat break_match; find_inversion; compute; auto. Qed.
imports: Verdi(Verdi HandlerMonad)