L : Language
L' : Language
M : Type w
N : Type ?u.238835
P : Type ?u.238838
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
φ✝ ψ : Formula L α
v✝ : α → M
φ : Formula L α
g : α → β
v : β → M
⊢ BoundedFormula.Realize φ (Sum.elim v (default ∘ ↑(Fin.cast (_ : 0 = 0))) ∘ Sum.inl ∘ g) (default ∘ ↑(natAdd 0)) =
    BoundedFormula.Realize φ (v ∘ g) default
L : Language
L' : Language
M : Type w
N : Type ?u.238835
P : Type ?u.238838
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
φ✝ ψ : Formula L α
v✝ : α → M
φ : Formula L α
g : α → β
v : β → M
⊢ Realize (relabel g φ) v ↔ Realize φ (v ∘ g)
rw [Realize, Realize, relabel, BoundedFormula.realize_relabel, iff_eq_eq, Fin.castAdd_zero]
no goals
L : Language
L' : Language
M : Type w
N : Type ?u.238835
P : Type ?u.238838
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
φ✝ ψ : Formula L α
v✝ : α → M
φ : Formula L α
g : α → β
v : β → M
⊢ BoundedFormula.Realize φ (Sum.elim v (default ∘ ↑(Fin.cast (_ : 0 = 0))) ∘ Sum.inl ∘ g) (default ∘ ↑(natAdd 0)) =
    BoundedFormula.Realize φ (v ∘ g) default
exact congr rfl (funext finZeroElim)