exact ⟨e, ⟨he, fun h => by simpa using hm _ h⟩, he⟩
case unit.mp.intro.intro
μ : Type ?u.1286883
L : Language
inst✝⁷ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁶ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁵ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Func
inst✝² : UniformlyPrimcodable L.Rel
inst✝¹ : Primcodable μ
T : Theory L
inst✝ : DecidablePred T
σ : Sentence L
h : ∃ e, isProofFn T σ e = true
e : ℕ
he : isProofFn T σ e = true
hm : ∀ z < e, ¬isProofFn T σ z = true
⊢ ∃ a, (isProofFn T σ a = true ∧ ∀ {m : ℕ}, m < a → isProofFn T σ m = false) ∧ isProofFn T σ a = true
no goals