Transcript count Q le of is Per Index Query Bound

theorem transcript_countQ_le_of_isPerIndexQueryBound (h : OracleHandler spec) [DecidableEq ι]    (t : ι) :    ∀ {oa : OracleComp spec α} {qb : ι → ℕ}, IsPerIndexQueryBound oa qb →      (transcript h oa).countQ (· = t) ≤ qb t := by  intro oa  induction oa with  | pure x => intro qb _; exact Nat.zero_le (qb t)  | queryBind t' k ih =>      intro qb hb      obtain ⟨hpos, hrest⟩ := hb      have hle := ih (h t') (hrest (h t'))      simp only [] at hpos hle      rw [transcript_countQ_queryBind]      rcases eq_or_ne t' t with rfl | htt      · rw [Function.update_self] at hle        split_ifs <;> omega      · rw [Function.update_of_ne htt.symm] at hle        simp only [if_neg htt]; omega