proposition: Lemma nwnw_lock : forall p p', pBody p = Lock -> LockServ_network_network_invariant p p'.
proof: Proof. Proof using. unfold LockServ_network_network_invariant. intuition; simpl in *; congruence. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)