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