fact: Definition contract_iso_rl `(c1 : contract i Ω1) `(c2 : contract i Ω2) (equ : contract_equ c1 c2) (ω2 : Ω2) : Ω1 := match equ with | @mk_contract_equ _ _ _ _ _ _ g _ _ _ _ _ => g ω2 end.
imports: Coq(Setoid Morphisms) ExtLib(StateMonad MonadState MonadTrans) FreeSpec.Core(Interface Impure Semantics Component)