Theorem: LO.FirstOrder.Arith.FirstIncompleteness.pred_representation (Logic/FirstOrder/Arith/Representation.lean)

State before:
T : Theory ℒₒᵣ
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : 𝐏𝐀⁻ ≼ T
inst✝⁵ : DecidablePred T
inst✝⁴ : SigmaOneSound T
inst✝³ : T.Computable
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
p : α → Prop
hp : RePred p
x : α
⊢ T ⊢! [→ ⸢x⸣].hom (pred p) ↔ p x
Tactic:
simpa [pred, ←Rew.hom_comp_app, Rew.substs_comp_substs] using
  representation hp (T := T) (x := x) (y := ())
State after:
no goals