Transcript count Q le of is Query Bound P

theorem transcript_countQ_le_of_isQueryBoundP (h : OracleHandler spec) (p : ι → Prop)    [DecidablePred p] :    ∀ {oa : OracleComp spec α} {n : ℕ}, IsQueryBoundP oa p n →      (transcript h oa).countQ p ≤ n := by  intro oa  induction oa with  | pure x => intro n _; exact Nat.zero_le n  | queryBind t k ih =>      intro n hb      obtain ⟨hp, hrest⟩ := hb      have hle := ih (h t) (hrest (h t))      simp only [] at hle      rw [transcript_countQ_queryBind]      by_cases hpt : p t      · have hn : 0 < n := hp.resolve_left (not_not_intro hpt)        simp only [hpt, if_true] at hle ⊢        omega      · simp only [hpt, if_false] at hle ⊢        omega