Fst map run simulate Q

theorem fst_map_run_simulateQ {oa : OracleComp spec α} {qb : ι → ℕ}    (h : IsPerIndexQueryBound oa qb) :    Prod.fst <$> (simulateQ enforceOracle oa).run qb = oa := by  induction oa using OracleComp.inductionOn generalizing qb with  | pure _ => simp  | query_bind t mx ih =>    rw [isPerIndexQueryBound_query_bind_iff] at h    obtain ⟨hpos, hcont⟩ := h    simp only [simulateQ_query_bind]    change Prod.fst <$> ((spec.enforceOracle t).run qb >>=      fun p => (simulateQ enforceOracle (mx p.1)).run p.2) = liftM (query t) >>= mx    rw [run_apply, if_pos hpos]    simp only [monad_norm, Function.comp]    exact bind_congr fun u => by      simpa only [map_eq_bind_pure_comp] using ih u (hcont u)