fact: Fixpoint revert_trace (tr : list (name * ((@input PB_base_params) + list (@output PB_base_params)))) : list (@input base_params * (@output base_params)) := match tr with | [] => [] | (h, t) :: tr' => match t with | inr l => filterMap (fun x => match x with | RequestResponse i os => Some (i, os) | _ => None end) l | _ => [] end ++ revert_trace tr' end.
imports: Verdi(Verdi HandlerMonad)