IND CPA run' eval Dist eq query Impl' of bounded eq

theorem IND_CPA_run'_evalDist_eq_queryImpl'_of_bounded_eq [Finite C] [Inhabited C]    (implCounted : PK → Bool → ℕ →      QueryImpl encAlg'.IND_CPA_oracleSpec (StateT encAlg'.IND_CPA_CountedState ProbComp))    (hsame : ∀ (pk : PK) (b : Bool) (realUntil : ℕ)      (t : encAlg'.IND_CPA_oracleSpec.Domain) (st : encAlg'.IND_CPA_CountedState),      (match t with | .inl _ => True | .inr _ => st.2 < realUntil) →      (encAlg'.IND_CPA_queryImpl'_counted pk b t).run st =        (implCounted pk b realUntil t).run st)    (pk : PK) (b : Bool) (q : ℕ)    {α : Type} (comp : OracleComp encAlg'.IND_CPA_oracleSpec α)    (budget : ℕ)    (hbound : comp.IsQueryBoundP (· matches .inr _) budget)    (cache : (M × M →ₒ C).QueryCache) (n : ℕ) (hn : n + budget ≤ q) :    𝒟[(simulateQ (implCounted pk b q) comp).run' (cache, n)] =      𝒟[(simulateQ (encAlg'.IND_CPA_queryImpl' pk b) comp).run' cache] := by  have hrun :      𝒟[(simulateQ (implCounted pk b q) comp).run (cache, n)] =      𝒟[(simulateQ (encAlg'.IND_CPA_queryImpl'_counted pk b) comp).run (cache, n)] := by    refine evalDist_ext fun z =>      OracleComp.ProgramLogic.Relational.probOutput_simulateQ_run_eq_of_impl_eq_queryBound        (impl₁ := implCounted pk b q) (impl₂ := encAlg'.IND_CPA_queryImpl'_counted pk b)        (Inv := fun st budget => st.2 + budget ≤ q)        (canQuery := fun t n => ¬ (Sum.isRight t = true) ∨ 0 < n)        (cost := fun t n => if Sum.isRight t = true then n - 1 else n)        (oa := comp) (budget := budget)        (hbound := (OracleComp.isQueryBoundP_congr_pred (fun t => by cases t <;> simp)).mp hbound)        (himpl_eq := fun t st budget hInv hcan => (hsame pk b q t st (by          cases t with          | inl _ => trivial          | inr _ => simp only [Sum.isRight, not_true, false_or] at hcan; omega)).symm)        (hpres₂ := IND_CPA_queryImpl'_counted_run_invariant_le pk b q)        (s := (cache, n)) (hs := hn) (z := z)  have hcounted_run' :      𝒟[(simulateQ (implCounted pk b q) comp).run' (cache, n)] =      𝒟[(simulateQ (encAlg'.IND_CPA_queryImpl'_counted pk b) comp).run'        (cache, n)] := by    simp only [StateT.run'_eq, evalDist_map]    exact congrArg (fun p => Prod.fst <$> p) hrun  refine hcounted_run'.trans ?_  simpa using congrArg evalDist (OracleComp.run'_simulateQ_eq_of_query_map_eq      (impl₁ := encAlg'.IND_CPA_queryImpl'_counted pk b)      (impl₂ := encAlg'.IND_CPA_queryImpl' pk b)      (proj := Prod.fst)      (hproj := encAlg'.IND_CPA_queryImpl'_counted_proj_eq_queryImpl' pk b)      comp (cache, n))