proposition: Lemma nwnw_sym : forall p q, LockServ_network_network_invariant p q -> LockServ_network_network_invariant q p.
proof: Proof. Proof using. unfold LockServ_network_network_invariant. intuition. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)