case var
L : Language
L' : Language
M : Type w
N : Type ?u.5460
P : Type ?u.5463
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_1
f : α → β
g : β → γ
_a✝ : α
⊢ relabel g (relabel f (var _a✝)) = relabel (g ∘ f) (var _a✝)

case func
L : Language
L' : Language
M : Type w
N : Type ?u.5460
P : Type ?u.5463
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_1
f : α → β
g : β → γ
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L α
ih : ∀ (a : Fin l✝), relabel g (relabel f (_ts✝ a)) = relabel (g ∘ f) (_ts✝ a)
⊢ relabel g (relabel f (func _f✝ _ts✝)) = relabel (g ∘ f) (func _f✝ _ts✝)
L : Language
L' : Language
M : Type w
N : Type ?u.5460
P : Type ?u.5463
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_1
f : α → β
g : β → γ
t : Term L α
⊢ relabel g (relabel f t) = relabel (g ∘ f) t
induction' t with _ _ _ _ ih
no goals
case var
L : Language
L' : Language
M : Type w
N : Type ?u.5460
P : Type ?u.5463
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_1
f : α → β
g : β → γ
_a✝ : α
⊢ relabel g (relabel f (var _a✝)) = relabel (g ∘ f) (var _a✝)
rfl
no goals
case func
L : Language
L' : Language
M : Type w
N : Type ?u.5460
P : Type ?u.5463
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_1
f : α → β
g : β → γ
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L α
ih : ∀ (a : Fin l✝), relabel g (relabel f (_ts✝ a)) = relabel (g ∘ f) (_ts✝ a)
⊢ relabel g (relabel f (func _f✝ _ts✝)) = relabel (g ∘ f) (func _f✝ _ts✝)
simp [ih]