no goals
L : Language
L' : Language
M : Type w
N : Type ?u.96990
P : Type ?u.96993
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ l : ℕ
φ✝ ψ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝ : Fin l → M
m n : ℕ
φ : BoundedFormula L α n
g : α → β ⊕ Fin m
v : β → M
xs : Fin (m + n) → M
⊢ Realize (relabel g φ) v xs ↔ Realize φ (Sum.elim v (xs ∘ ↑(castAdd n)) ∘ g) (xs ∘ ↑(natAdd m))
rw [relabel, realize_mapTermRel_add_castLe] <;> intros <;> simp