exact ⟨e, he⟩
case unit.mpr.intro.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
e : ℕ
right✝¹ he : isProofFn T σ e = true
right✝ : ∀ {m : ℕ}, m < e → isProofFn T σ m = false
⊢ ∃ e, isProofFn T σ e = true
no goals