Simulate Q triple preserves invariant

theorem simulateQ_triple_preserves_invariant {σ α : Type}    (handler : QueryImpl spec (StateT σ (OracleComp spec)))    (I : σ → Prop)    (hhandler : ∀ t : spec.Domain, Std.Do.Triple (handler t)      (spred(fun s => ⌜I s⌝))      (⇓ _ s' => ⌜I s'⌝))    (oa : OracleComp spec α) :    Std.Do.Triple      (simulateQ handler oa : StateT σ (OracleComp spec) α)      (spred(fun s => ⌜I s⌝))      (⇓ _ s' => ⌜I s'⌝) := by  -- A pure `Std.Do`-level proof via `Triple.pure` / `Triple.bind` is the  -- structurally right thing, but consistently times out on `isDefEq` in  -- the `query_bind` step (verified up to 1M heartbeats with several  -- variations: explicit `R`, explicit `Q`, stripping `liftM` via  -- `simulateQ_bind` + `simulateQ_query` + `id_map`). The cost appears to  -- be in `(wp x).mono` reduction inside `Triple.bind` for the  -- `StateT σ (OracleComp spec)` instance; this is plausibly a `Std.Do`  -- upstream issue worth reporting.  --  -- For now, bail out once to the support layer and induct directly on  -- `oa`. Downstream consumers stay in the `Std.Do` world.  rw [triple_stateT_iff_forall_support]  induction oa using OracleComp.inductionOn with  | pure x =>    intro s hs a s' hmem    simp only [simulateQ_pure, StateT.run_pure, support_pure, Set.mem_singleton_iff,      Prod.mk.injEq] at hmem    obtain ⟨_, hseq⟩ := hmem    exact hseq ▸ hs  | query_bind t oa ih =>    intro s hs a s' hmem    simp only [simulateQ_query_bind, OracleQuery.input_query,      StateT.run_bind, support_bind, Set.mem_iUnion] at hmem    obtain ⟨⟨u, s₁⟩, hmem₁, hmem₂⟩ := hmem    have hhand := hhandler t    rw [triple_stateT_iff_forall_support] at hhand    exact ih u s₁ (hhand s hs u s₁ hmem₁) a s' hmem₂