proposition: Theorem transformer : forall (P : list (input * output) -> Prop), (forall st tr, step_1_star init st tr -> P tr) -> (forall net tr, step_async_star step_async_init net tr -> P (revert_trace tr)).
proof: Proof. Proof using. intros. find_apply_lem_hyp simulation. eauto. Qed.
imports: Verdi(Verdi HandlerMonad)