Is Query Bound P lift Comp sub Spec

theorem IsQueryBoundP.liftComp_subSpec    [h : spec ⊂ₒ superSpec]    {oa : OracleComp spec α}    {p : spec.Domain → Prop} [DecidablePred p]    {q : superSpec.Domain → Prop} [DecidablePred q]    {n : ℕ}    (hpq : ∀ t, p t ↔ q (h.onQuery t))    (hoa : oa.IsQueryBoundP p n) :    (liftComp oa superSpec).IsQueryBoundP q n := by  induction oa using OracleComp.inductionOn generalizing n with  | pure x => simp  | query_bind t mx ih =>      rw [isQueryBoundP_query_bind_iff] at hoa      rw [liftComp_bind, liftComp_query]      change IsQueryBoundP        ((liftM (spec.query t) : OracleComp superSpec (spec.Range t)) >>=          fun u => liftComp (mx u) superSpec) q n      rw [show          (liftM (spec.query t) : OracleComp superSpec (spec.Range t)) =            liftM (superSpec.query (h.onQuery t)) >>= fun u =>              pure (h.onResponse t u) by        change ((liftM (spec.query t) : OracleQuery superSpec (spec.Range t)) :            OracleComp superSpec (spec.Range t)) =          (liftM (superSpec.query (h.onQuery t)) >>= fun u =>            pure (h.onResponse t u))        rw [show            (liftM (spec.query t) : OracleQuery superSpec (spec.Range t)) =              ⟨h.onQuery t, h.onResponse t⟩ from h.liftM_eq_lift _]        rfl]      rw [bind_assoc, isQueryBoundP_query_bind_iff]      refine ⟨by simpa [← hpq t] using hoa.1, fun u => ?_⟩      rw [pure_bind]      have hcont := ih (h.onResponse t u) (hoa.2 (h.onResponse t u))      by_cases hp : p t      · simpa [hp, (hpq t).1 hp] using hcont      · simpa [hp, mt (hpq t).2 hp] using hcont