case h
L : Language
L' : Language
M : Type w
N : Type ?u.28071
P : Type ?u.28074
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.28102
t : Term L α
⊢ onTerm (LHom.id L) t = id t
L : Language
L' : Language
M : Type w
N : Type ?u.28071
P : Type ?u.28074
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.28102
⊢ onTerm (LHom.id L) = id
ext t
case h.var
L : Language
L' : Language
M : Type w
N : Type ?u.28071
P : Type ?u.28074
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.28102
_a✝ : α
⊢ onTerm (LHom.id L) (var _a✝) = id (var _a✝)

case h.func
L : Language
L' : Language
M : Type w
N : Type ?u.28071
P : Type ?u.28074
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.28102
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L α
ih : ∀ (a : Fin l✝), onTerm (LHom.id L) (_ts✝ a) = id (_ts✝ a)
⊢ onTerm (LHom.id L) (func _f✝ _ts✝) = id (func _f✝ _ts✝)
case h
L : Language
L' : Language
M : Type w
N : Type ?u.28071
P : Type ?u.28074
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.28102
t : Term L α
⊢ onTerm (LHom.id L) t = id t
induction' t with _ _ _ _ ih
no goals
case h.var
L : Language
L' : Language
M : Type w
N : Type ?u.28071
P : Type ?u.28074
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.28102
_a✝ : α
⊢ onTerm (LHom.id L) (var _a✝) = id (var _a✝)
rfl
case h.func
L : Language
L' : Language
M : Type w
N : Type ?u.28071
P : Type ?u.28074
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.28102
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L α
ih : ∀ (a : Fin l✝), onTerm (LHom.id L) (_ts✝ a) = id (_ts✝ a)
⊢ (func (onFunction (LHom.id L) _f✝) fun i => id (_ts✝ i)) = id (func _f✝ _ts✝)
case h.func
L : Language
L' : Language
M : Type w
N : Type ?u.28071
P : Type ?u.28074
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.28102
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L α
ih : ∀ (a : Fin l✝), onTerm (LHom.id L) (_ts✝ a) = id (_ts✝ a)
⊢ onTerm (LHom.id L) (func _f✝ _ts✝) = id (func _f✝ _ts✝)
simp_rw [onTerm, ih]
no goals
case h.func
L : Language
L' : Language
M : Type w
N : Type ?u.28071
P : Type ?u.28074
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.28102
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L α
ih : ∀ (a : Fin l✝), onTerm (LHom.id L) (_ts✝ a) = id (_ts✝ a)
⊢ (func (onFunction (LHom.id L) _f✝) fun i => id (_ts✝ i)) = id (func _f✝ _ts✝)
rfl