fact: Definition input_key (i : input) : key := match i with | Get k => k | Put k _ => k | Del k => k | CAS k _ _ => k | CAD k _ => k end.
imports: Verdi(Verdi) Coq(FMapList String) Verdi(FMapVeryWeak StateMachineHandlerMonad)