fact: Example revert_trace_eg : forall net tr o, step_async_star (params := PB_multi_params) step_async_init net tr -> inputs_m tr = [Put "james" "awesome"] -> outputs_m tr = [o] -> o = Response "james" (Some "awesome") None.
imports: Verdi(Verdi) Coq(String) Verdi(VarD PrimaryBackup)