proposition: Lemma decomposition_reachable_nw_invariant : forall st tr p, step_async_star step_async_init st tr -> In p (nwPackets st) -> network_invariant (nwState st) p.
proof: Proof. Proof using. pose proof decomposition_invariant. find_apply_lem_hyp inductive_invariant_true_in_reachable. unfold true_in_reachable, reachable in *. intuition. unfold composed_invariant in *. apply H; eauto. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)