proposition: Lemma locks_correct_implies_mutex : forall sigma, locks_correct sigma -> mutual_exclusion sigma.
proof: Proof. Proof using. unfold locks_correct, mutual_exclusion. intros. repeat find_apply_hyp_hyp. break_exists. find_rewrite. find_inversion. auto. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)