case var
L : Language
M : Type u_4
s : Setoid M
ps : Prestructure L s
β : Type u_1
x : β → M
_a✝ : β
⊢ realize (fun i => Quotient.mk s (x i)) (var _a✝) = Quotient.mk s (realize x (var _a✝))

case func
L : Language
M : Type u_4
s : Setoid M
ps : Prestructure L s
β : Type u_1
x : β → M
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L β
ih : ∀ (a : Fin l✝), realize (fun i => Quotient.mk s (x i)) (_ts✝ a) = Quotient.mk s (realize x (_ts✝ a))
⊢ realize (fun i => Quotient.mk s (x i)) (func _f✝ _ts✝) = Quotient.mk s (realize x (func _f✝ _ts✝))
L : Language
M : Type u_4
s : Setoid M
ps : Prestructure L s
β : Type u_1
t : Term L β
x : β → M
⊢ realize (fun i => Quotient.mk s (x i)) t = Quotient.mk s (realize x t)
induction' t with _ _ _ _ ih
no goals
case var
L : Language
M : Type u_4
s : Setoid M
ps : Prestructure L s
β : Type u_1
x : β → M
_a✝ : β
⊢ realize (fun i => Quotient.mk s (x i)) (var _a✝) = Quotient.mk s (realize x (var _a✝))
rfl
no goals
case func
L : Language
M : Type u_4
s : Setoid M
ps : Prestructure L s
β : Type u_1
x : β → M
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L β
ih : ∀ (a : Fin l✝), realize (fun i => Quotient.mk s (x i)) (_ts✝ a) = Quotient.mk s (realize x (_ts✝ a))
⊢ realize (fun i => Quotient.mk s (x i)) (func _f✝ _ts✝) = Quotient.mk s (realize x (func _f✝ _ts✝))
simp only [ih, funMap_quotient_mk', Term.realize]