proposition: Lemma nwnw_unlock_lock : forall p q, LockServ_network_network_invariant p q -> pBody p = Unlock -> pBody q = Lock.
proof: Proof. Proof using. unfold LockServ_network_network_invariant. intros. destruct (pBody q); intuition; try discriminate. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)