case var
L : Language
L' : Language
M : Type w
N : Type ?u.1019
P : Type ?u.1022
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
g : α → β
v : β → M
_a✝ : α
⊢ realize v (relabel g (var _a✝)) = realize (v ∘ g) (var _a✝)

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