proposition: Lemma locks_correct_invariant : forall st, reachable step_async step_async_init st -> locks_correct (nwState st).
proof: Proof. Proof using. intros. pose proof decomposition_invariant. find_apply_lem_hyp inductive_invariant_true_in_reachable. unfold true_in_reachable in *. apply H0; auto. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)