case h
L : Language
L' : Language
M : Type w
N : Type ?u.143751
P : Type ?u.143754
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.143782
n : ℕ
f : BoundedFormula L α n
⊢ onBoundedFormula (LHom.id L) f = id f
L : Language
L' : Language
M : Type w
N : Type ?u.143751
P : Type ?u.143754
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.143782
n : ℕ
⊢ onBoundedFormula (LHom.id L) = id
ext f
case h.falsum
L : Language
L' : Language
M : Type w
N : Type ?u.143751
P : Type ?u.143754
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.143782
n n✝ : ℕ
⊢ onBoundedFormula (LHom.id L) falsum = id falsum

case h.equal
L : Language
L' : Language
M : Type w
N : Type ?u.143751
P : Type ?u.143754
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.143782
n n✝ : ℕ
t₁✝ t₂✝ : Term L (α ⊕ Fin n✝)
⊢ onBoundedFormula (LHom.id L) (equal t₁✝ t₂✝) = id (equal t₁✝ t₂✝)

case h.rel
L : Language
L' : Language
M : Type w
N : Type ?u.143751
P : Type ?u.143754
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.143782
n n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (α ⊕ Fin n✝)
⊢ onBoundedFormula (LHom.id L) (rel R✝ ts✝) = id (rel R✝ ts✝)

case h.imp
L : Language
L' : Language
M : Type w
N : Type ?u.143751
P : Type ?u.143754
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.143782
n n✝ : ℕ
f₁✝ f₂✝ : BoundedFormula L α n✝
ih1 : onBoundedFormula (LHom.id L) f₁✝ = id f₁✝
ih2 : onBoundedFormula (LHom.id L) f₂✝ = id f₂✝
⊢ onBoundedFormula (LHom.id L) (imp f₁✝ f₂✝) = id (imp f₁✝ f₂✝)

case h.all
L : Language
L' : Language
M : Type w
N : Type ?u.143751
P : Type ?u.143754
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.143782
n n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih3 : onBoundedFormula (LHom.id L) f✝ = id f✝
⊢ onBoundedFormula (LHom.id L) (all f✝) = id (all f✝)
case h
L : Language
L' : Language
M : Type w
N : Type ?u.143751
P : Type ?u.143754
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.143782
n : ℕ
f : BoundedFormula L α n
⊢ onBoundedFormula (LHom.id L) f = id f
induction' f with _ _ _ _ _ _ _ _ _ _ _ ih1 ih2 _ _ ih3
no goals
case h.falsum
L : Language
L' : Language
M : Type w
N : Type ?u.143751
P : Type ?u.143754
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.143782
n n✝ : ℕ
⊢ onBoundedFormula (LHom.id L) falsum = id falsum
rfl
no goals
case h.equal
L : Language
L' : Language
M : Type w
N : Type ?u.143751
P : Type ?u.143754
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.143782
n n✝ : ℕ
t₁✝ t₂✝ : Term L (α ⊕ Fin n✝)
⊢ onBoundedFormula (LHom.id L) (equal t₁✝ t₂✝) = id (equal t₁✝ t₂✝)
rw [onBoundedFormula, LHom.id_onTerm, id.def, id.def, id.def, Term.bdEqual]
case h.rel
L : Language
L' : Language
M : Type w
N : Type ?u.143751
P : Type ?u.143754
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.143782
n n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (α ⊕ Fin n✝)
⊢ Relations.boundedFormula (onRelation (LHom.id L) R✝) (id ∘ ts✝) = id (rel R✝ ts✝)
case h.rel
L : Language
L' : Language
M : Type w
N : Type ?u.143751
P : Type ?u.143754
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.143782
n n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (α ⊕ Fin n✝)
⊢ onBoundedFormula (LHom.id L) (rel R✝ ts✝) = id (rel R✝ ts✝)
rw [onBoundedFormula, LHom.id_onTerm]
no goals
case h.rel
L : Language
L' : Language
M : Type w
N : Type ?u.143751
P : Type ?u.143754
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.143782
n n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (α ⊕ Fin n✝)
⊢ Relations.boundedFormula (onRelation (LHom.id L) R✝) (id ∘ ts✝) = id (rel R✝ ts✝)
rfl
no goals
case h.imp
L : Language
L' : Language
M : Type w
N : Type ?u.143751
P : Type ?u.143754
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.143782
n n✝ : ℕ
f₁✝ f₂✝ : BoundedFormula L α n✝
ih1 : onBoundedFormula (LHom.id L) f₁✝ = id f₁✝
ih2 : onBoundedFormula (LHom.id L) f₂✝ = id f₂✝
⊢ onBoundedFormula (LHom.id L) (imp f₁✝ f₂✝) = id (imp f₁✝ f₂✝)
rw [onBoundedFormula, ih1, ih2, id.def, id.def, id.def]
no goals
case h.all
L : Language
L' : Language
M : Type w
N : Type ?u.143751
P : Type ?u.143754
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.143782
n n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih3 : onBoundedFormula (LHom.id L) f✝ = id f✝
⊢ onBoundedFormula (LHom.id L) (all f✝) = id (all f✝)
rw [onBoundedFormula, ih3, id.def, id.def]