proposition: Lemma mutual_exclusion_invariant : forall st, reachable step_async step_async_init st -> mutual_exclusion (nwState st).
proof: Proof. Proof using. intros. apply locks_correct_implies_mutex. auto using locks_correct_invariant. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)