Theorem: LO.FirstOrder.not_fvar?_newVar (Logic/FirstOrder/Completeness/Coding.lean)

State before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
p : SyntacticFormula L
Γ : Sequent L
h : p ∈ Γ
⊢ upper p ≤ newVar Γ
Tactic:
simpa[newVar] using List.le_max_of_le (List.mem_map_of_mem _ h) (by simp)
State after:
no goals

State before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
p : SyntacticFormula L
Γ : Sequent L
h : p ∈ Γ
⊢ upper p ≤ upper p
Tactic:
simp
State after:
no goals