proposition: Lemma reachable_intro : forall a tr, step_async_star step_async_init a tr -> reachable step_async step_async_init a.
proof: Proof. Proof using. unfold reachable. intros. eauto. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)