fact: Definition sharedcontractprod `{Provide ix i, Provide ix j} `(ci : contract i Ω) (cj : contract j Ω) : contract ix Ω := {| witness_update := fun (ω : Ω) (α : Type) (e : ix α) (x : α) => match proj_p (i:=i) e with | Some e => witness_update ci ω e x | _ => match proj_p (i:=j) e with | Some e => witness_update cj ω e x | _ => ω end end; caller_obligation := fun (ω : Ω) (α : Type) (e : ix α) => gen_caller_obligation ci ω e /\ gen_caller_obligation cj ω e; callee_obligation := fun (ω : Ω) (α : Type) (e : ix α) (x : α) => gen_callee_obligation ci ω e x /\ gen_callee_obligation cj ω e x |}.
imports: Coq(Setoid Morphisms) ExtLib(StateMonad MonadState MonadTrans) FreeSpec.Core(Interface Impure Semantics Component)