proposition: Lemma LockServ_nwnw_input_handlers_new_new : forall h i sigma u st' out ms, InputHandler h i (sigma h) = (u, out, st', ms) -> distinct_pairs_and LockServ_network_network_invariant (map (fun m => mkPacket h (fst m) (snd m)) ms).
proof: Proof. Proof using. set_up_input_handlers. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)