proposition: Lemma network_invariant_inductive : forall net net' tr, step_async net net' tr -> network_invariant net -> network_invariant net'.
proof: Proof. Proof using. intros. invc H; simpl in *. - unfold network_invariant in *. simpl. find_apply_lem_hyp PB_net_defn'. workhorse; auto; intuition eauto. - unfold network_invariant in *. simpl. find_apply_lem_hyp PB_input_handler_defn. workhorse; auto; intuition eauto. Qed.
imports: Verdi(Verdi HandlerMonad)