L : Language
L' : Language
M : Type w
N : Type ?u.70714
P : Type ?u.70717
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 : ℕ
φ : BoundedFormula L α m
v : α → M
h' : m ≤ m
xs : Fin m → M
⊢ Realize (castLE h' φ) v xs ↔ Realize φ v (xs ∘ ↑(Fin.cast (_ : m = m)))
L : Language
L' : Language
M : Type w
N : Type ?u.70714
P : Type ?u.70717
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 : ℕ
h : m = n
h' : m ≤ n
φ : BoundedFormula L α m
v : α → M
xs : Fin n → M
⊢ Realize (castLE h' φ) v xs ↔ Realize φ v (xs ∘ ↑(Fin.cast h))
subst h
no goals
L : Language
L' : Language
M : Type w
N : Type ?u.70714
P : Type ?u.70717
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 : ℕ
φ : BoundedFormula L α m
v : α → M
h' : m ≤ m
xs : Fin m → M
⊢ Realize (castLE h' φ) v xs ↔ Realize φ v (xs ∘ ↑(Fin.cast (_ : m = m)))
simp only [castLE_rfl, cast_refl, OrderIso.coe_refl, Function.comp.right_id]