proposition: Theorem true_in_reachable_mutual_exclusion : true_in_reachable step_async step_async_init (fun net => mutual_exclusion (nwState net)).
proof: Proof. Proof using. pose proof decomposition_invariant. find_apply_lem_hyp inductive_invariant_true_in_reachable. unfold true_in_reachable in *. intros. apply locks_correct_implies_mutex. match goal with | [ H : _ |- _ ] => apply H end. auto. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)