proposition: Lemma correspond_Prefix : forall st net tr_1 tr_m, correspond st (nwState net) tr_1 tr_m -> Prefix (outputs_m tr_m) (outputs_1 tr_1).
proof: Proof. Proof using. unfold correspond. intros. break_let. intuition. subst. eauto using app_Prefix. Qed.
imports: Verdi(Verdi HandlerMonad)