fact: Definition gen_witness_update `{MayProvide ix i} {Ω α} (c : contract i Ω) (ω : Ω) (e : ix α) (x : α) : Ω := match proj_p e with | Some e => witness_update c ω e x | None => ω end.
imports: Coq(Setoid Morphisms) ExtLib(StateMonad MonadState MonadTrans) FreeSpec.Core(Interface Impure Semantics Component)