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