fact: Definition inputs_with_key (trace : list (input * output)) (k : key) : list input := filterMap (fun ev => if key_eq_dec k (input_key (fst ev)) then Some (fst ev) else None) trace.
imports: Verdi(Verdi) Coq(FMapList String) Verdi(FMapVeryWeak StateMachineHandlerMonad)