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

theorem OracleComp.mem_support_of_mem_support_liftComp {ι τ α : Type} {spec : OracleSpec ι} {superSpec : OracleSpec τ} [MonadLiftT (OracleQuery spec) (OracleQuery superSpec)] (oa : OracleComp spec α) (x : α) : x ∈ support (oa.liftComp superSpec) → x ∈ support oa

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

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)