intro σ
μ : Type ?u.1325212
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
inst✝ : T.Computable
⊢ ∀ (n : Sentence L), provableFn T n = Part.assert ((fun x => T ⊢! x) n) fun x => Part.some ()
μ : Type ?u.1325212
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
inst✝ : T.Computable
σ : Sentence L
⊢ provableFn T σ = Part.assert ((fun x => T ⊢! x) σ) fun x => Part.some ()