no goals
L : Language
L' : Language
M : Type w
N : Type ?u.115821
P : Type ?u.115824
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.115852
n l : ℕ
φ✝¹ ψ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
m : ℕ
φ : BoundedFormula L α m
h✝ : IsPrenex φ
f : α → β ⊕ Fin n
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
x✝ : IsPrenex φ✝
h : IsPrenex (BoundedFormula.relabel f φ✝)
⊢ IsPrenex (BoundedFormula.relabel f (BoundedFormula.all φ✝))
simp [h.all]
no goals
L : Language
L' : Language
M : Type w
N : Type ?u.115821
P : Type ?u.115824
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.115852
n l : ℕ
φ✝¹ ψ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
m : ℕ
φ : BoundedFormula L α m
h✝ : IsPrenex φ
f : α → β ⊕ Fin n
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
x✝ : IsPrenex φ✝
h : IsPrenex (BoundedFormula.relabel f φ✝)
⊢ IsPrenex (BoundedFormula.relabel f (BoundedFormula.ex φ✝))
simp [h.ex]