no goals
L : Language
L' : Language
M : Type w
N : Type ?u.239536
P : Type ?u.239539
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
φ✝ ψ : Formula L α
v✝ : α → M
φ : Formula L (Fin n)
v : Empty → M
x : Fin n → M
⊢ BoundedFormula.Realize (BoundedFormula.relabel Sum.inr φ) v x ↔ Realize φ x
rw [BoundedFormula.realize_relabel, Formula.Realize, Sum.elim_comp_inr, Fin.castAdd_zero,
  cast_refl, OrderIso.coe_refl, Function.comp.right_id,
  Subsingleton.elim (x ∘ (natAdd n : Fin 0 → Fin n)) default]