Theorem: LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.provableSentence_representation (Logic/FirstOrder/Incompleteness/SelfReference.lean)

State before:
T : Theory ℒₒᵣ
inst✝¹⁰ : 𝐄𝐐 ≼ T
inst✝⁹ : 𝐏𝐀⁻ ≼ T
inst✝⁸ : SigmaOneSound T
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
U : Theory L
inst✝¹ : DecidablePred U
inst✝ : U.Computable
σ : Sentence L
⊢ T ⊢! [→ ⸢σ⸣].hom (provableSentence U) ↔ U ⊢! σ
Tactic:
simpa using pred_representation (T := T) (provable_RePred U) (x := σ)
State after:
no goals