proposition: Lemma contract_equ_refl `(c : contract i Ω) : contract_equ c c.
proof: Proof. apply mk_contract_equ with (f:=fun x => x) (g:=fun x => x); auto. + now intros ω α p. + now intros ω α p x. + now intros ω α p x. Defined.
imports: Coq(Setoid Morphisms) ExtLib(StateMonad MonadState MonadTrans) FreeSpec.Core(Interface Impure Semantics Component)