Cache entry in log or initial

theorem cache_entry_in_log_or_initial {α : Type}    (oa : OracleComp spec α)    (cache₀ : QueryCache spec)    (z : (α × QueryLog spec) × QueryCache spec)    (hmem : z ∈ support ((simulateQ cachingOracle        ((simulateQ loggingOracle oa).run)).run cache₀)) :    ∀ (t₀ : spec.Domain) (v : spec.Range t₀),      z.2 t₀ = some v → cache₀ t₀ = some v ∨        ∃ entry ∈ z.1.2, entry.1 = t₀ ∧ HEq entry.2 v := by  induction oa using OracleComp.inductionOn generalizing cache₀ z with  | pure a =>    simp only [simulateQ_pure] at hmem    change z ∈ support (pure ((a, ([] : QueryLog spec)), cache₀)) at hmem    rw [support_pure, Set.mem_singleton_iff] at hmem    subst hmem    intro t₀ v hcache    exact Or.inl hcache  | query_bind t mx ih =>    obtain ⟨u, cache_mid, ⟨⟨x', log'⟩, cache_final⟩,      _, hcache_mid_entry, hcache_mid_eq, hmem_cont, rfl⟩ :=      exists_cont_of_run_simulateQ_query_bind t mx cache₀ z hmem    intro t₀ v hcache_final    rcases ih u cache_mid ((x', log'), cache_final) hmem_cont t₀ v hcache_final with      h_in_mid | ⟨entry, hentry, hentry_eq, hentry_heq⟩    · by_cases ht₀ : t₀ = t      · subst ht₀        rw [hcache_mid_entry] at h_in_mid; cases h_in_mid        exact Or.inr ⟨⟨t₀, _⟩, List.Mem.head _, rfl, HEq.rfl⟩      · exact Or.inl (hcache_mid_eq t₀ ht₀ ▸ h_in_mid)    · exact Or.inr ⟨entry, List.Mem.tail _ hentry, hentry_eq, hentry_heq⟩