case var
L : Language
L' : Language
M : Type w
N : Type ?u.7876
P : Type ?u.7879
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
tf : α → Term L β
v : β → M
_a✝ : α
⊢ realize v (subst (var _a✝) tf) = realize (fun a => realize v (tf a)) (var _a✝)

case func
L : Language
L' : Language
M : Type w
N : Type ?u.7876
P : Type ?u.7879
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
tf : α → Term L β
v : β → M
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L α
ih : ∀ (a : Fin l✝), realize v (subst (_ts✝ a) tf) = realize (fun a => realize v (tf a)) (_ts✝ a)
⊢ realize v (subst (func _f✝ _ts✝) tf) = realize (fun a => realize v (tf a)) (func _f✝ _ts✝)
L : Language
L' : Language
M : Type w
N : Type ?u.7876
P : Type ?u.7879
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
t : Term L α
tf : α → Term L β
v : β → M
⊢ realize v (subst t tf) = realize (fun a => realize v (tf a)) t
induction' t with _ _ _ _ ih
no goals
case var
L : Language
L' : Language
M : Type w
N : Type ?u.7876
P : Type ?u.7879
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
tf : α → Term L β
v : β → M
_a✝ : α
⊢ realize v (subst (var _a✝) tf) = realize (fun a => realize v (tf a)) (var _a✝)
rfl
no goals
case func
L : Language
L' : Language
M : Type w
N : Type ?u.7876
P : Type ?u.7879
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
tf : α → Term L β
v : β → M
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L α
ih : ∀ (a : Fin l✝), realize v (subst (_ts✝ a) tf) = realize (fun a => realize v (tf a)) (_ts✝ a)
⊢ realize v (subst (func _f✝ _ts✝) tf) = realize (fun a => realize v (tf a)) (func _f✝ _ts✝)
simp [ih]