fact: CoFixpoint semprod {i j} (sem_i : semantics i) (sem_j : semantics j) : semantics (i + j) := mk_semantics (fun _ e => match e with | in_left e => let (x, out) := run_effect sem_i e in (x, semprod out sem_j) | in_right e => let (x, out) := run_effect sem_j e in (x, semprod sem_i out) end).
imports: Coq(Program Setoid Morphisms) ExtLib(Monad StateMonad)