fact: Definition contract_witness_equ `(c1 : contract i Ω1) `(c2 : contract i Ω2) (f : Ω1 -> Ω2) : Prop := forall ω1 a (p : i a) x, f (witness_update c1 ω1 p x) = witness_update c2 (f ω1) p x.
imports: Coq(Setoid Morphisms) ExtLib(StateMonad MonadState MonadTrans) FreeSpec.Core(Interface Impure Semantics Component)