no goals
L : Language
L' : Language
M : Type w
N : Type ?u.97781
P : Type ?u.97784
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.97812
n : ℕ
g : α → β ⊕ Fin n
k : ℕ
φ : BoundedFormula L α (k + 1)
⊢ relabel g (BoundedFormula.ex φ) = BoundedFormula.ex (relabel g φ)
simp [BoundedFormula.ex]