Additions to VCV-io's OracleComp.Coercions.SubSpec

theorem OracleComp.bind_liftComp_map {ι τ α β γ : Type} {spec : OracleSpec ι} {superSpec : OracleSpec τ} [MonadLiftT (OracleQuery spec) (OracleQuery superSpec)] (oa : OracleComp spec α) (f : α → β) (body : β → OracleComp superSpec γ) : (do let b ← f <$> oa.liftComp superSpec body b) = do let a ← oa.liftComp superSpec body (f a)