case var
L : Language
L' : Language
M : Type w
N : Type ?u.5062
P : Type ?u.5065
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.5093
_a✝ : α
⊢ relabel id (var _a✝) = var _a✝

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