case falsum
L : Language
L' : Language
M : Type w
N : Type ?u.48561
P : Type ?u.48564
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.48592
n✝¹ n : ℕ
h✝ : n ≤ n
n✝ : ℕ
h : n✝ ≤ n✝
⊢ castLE h falsum = falsum

case equal
L : Language
L' : Language
M : Type w
N : Type ?u.48561
P : Type ?u.48564
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.48592
n✝¹ n : ℕ
h✝ : n ≤ n
n✝ : ℕ
t₁✝ t₂✝ : Term L (α ⊕ Fin n✝)
h : n✝ ≤ n✝
⊢ castLE h (equal t₁✝ t₂✝) = equal t₁✝ t₂✝

case rel
L : Language
L' : Language
M : Type w
N : Type ?u.48561
P : Type ?u.48564
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.48592
n✝¹ n : ℕ
h✝ : n ≤ n
n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (α ⊕ Fin n✝)
h : n✝ ≤ n✝
⊢ castLE h (rel R✝ ts✝) = rel R✝ ts✝

case imp
L : Language
L' : Language
M : Type w
N : Type ?u.48561
P : Type ?u.48564
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.48592
n✝¹ n : ℕ
h✝ : n ≤ n
n✝ : ℕ
f₁✝ f₂✝ : BoundedFormula L α n✝
ih1 : ∀ (h : n✝ ≤ n✝), castLE h f₁✝ = f₁✝
ih2 : ∀ (h : n✝ ≤ n✝), castLE h f₂✝ = f₂✝
h : n✝ ≤ n✝
⊢ castLE h (imp f₁✝ f₂✝) = imp f₁✝ f₂✝

case all
L : Language
L' : Language
M : Type w
N : Type ?u.48561
P : Type ?u.48564
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.48592
n✝¹ n : ℕ
h✝ : n ≤ n
n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih3 : ∀ (h : n✝ + 1 ≤ n✝ + 1), castLE h f✝ = f✝
h : n✝ ≤ n✝
⊢ castLE h (all f✝) = all f✝
L : Language
L' : Language
M : Type w
N : Type ?u.48561
P : Type ?u.48564
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.48592
n✝ n : ℕ
h : n ≤ n
φ : BoundedFormula L α n
⊢ castLE h φ = φ
induction' φ with _ _ _ _ _ _ _ _ _ _ _ ih1 ih2 _ _ ih3
no goals
case falsum
L : Language
L' : Language
M : Type w
N : Type ?u.48561
P : Type ?u.48564
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.48592
n✝¹ n : ℕ
h✝ : n ≤ n
n✝ : ℕ
h : n✝ ≤ n✝
⊢ castLE h falsum = falsum
rfl
no goals
case equal
L : Language
L' : Language
M : Type w
N : Type ?u.48561
P : Type ?u.48564
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.48592
n✝¹ n : ℕ
h✝ : n ≤ n
n✝ : ℕ
t₁✝ t₂✝ : Term L (α ⊕ Fin n✝)
h : n✝ ≤ n✝
⊢ castLE h (equal t₁✝ t₂✝) = equal t₁✝ t₂✝
simp [Fin.castLE_of_eq]
no goals
case rel
L : Language
L' : Language
M : Type w
N : Type ?u.48561
P : Type ?u.48564
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.48592
n✝¹ n : ℕ
h✝ : n ≤ n
n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (α ⊕ Fin n✝)
h : n✝ ≤ n✝
⊢ castLE h (rel R✝ ts✝) = rel R✝ ts✝
simp [Fin.castLE_of_eq]
no goals
case imp
L : Language
L' : Language
M : Type w
N : Type ?u.48561
P : Type ?u.48564
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.48592
n✝¹ n : ℕ
h✝ : n ≤ n
n✝ : ℕ
f₁✝ f₂✝ : BoundedFormula L α n✝
ih1 : ∀ (h : n✝ ≤ n✝), castLE h f₁✝ = f₁✝
ih2 : ∀ (h : n✝ ≤ n✝), castLE h f₂✝ = f₂✝
h : n✝ ≤ n✝
⊢ castLE h (imp f₁✝ f₂✝) = imp f₁✝ f₂✝
simp [Fin.castLE_of_eq, ih1, ih2]
no goals
case all
L : Language
L' : Language
M : Type w
N : Type ?u.48561
P : Type ?u.48564
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.48592
n✝¹ n : ℕ
h✝ : n ≤ n
n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih3 : ∀ (h : n✝ + 1 ≤ n✝ + 1), castLE h f✝ = f✝
h : n✝ ≤ n✝
⊢ castLE h (all f✝) = all f✝
simp [Fin.castLE_of_eq, ih3]