case var
L : Language
L' : Language
M : Type w
N : Type ?u.9538
P : Type ?u.9541
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
inst✝ : DecidableEq α
t : Term L α
s : Set α
h✝ : ↑(varFinset t) ⊆ s
v : α → M
_a✝ : α
h : ↑(varFinset (var _a✝)) ⊆ s
⊢ realize (v ∘ Subtype.val) (restrictVar (var _a✝) (Set.inclusion h)) = realize v (var _a✝)

case func
L : Language
L' : Language
M : Type w
N : Type ?u.9538
P : Type ?u.9541
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
inst✝ : DecidableEq α
t : Term L α
s : Set α
h✝ : ↑(varFinset t) ⊆ s
v : α → M
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L α
ih :
  ∀ (a : Fin l✝) (h : ↑(varFinset (_ts✝ a)) ⊆ s),
    realize (v ∘ Subtype.val) (restrictVar (_ts✝ a) (Set.inclusion h)) = realize v (_ts✝ a)
h : ↑(varFinset (func _f✝ _ts✝)) ⊆ s
⊢ realize (v ∘ Subtype.val) (restrictVar (func _f✝ _ts✝) (Set.inclusion h)) = realize v (func _f✝ _ts✝)
L : Language
L' : Language
M : Type w
N : Type ?u.9538
P : Type ?u.9541
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
inst✝ : DecidableEq α
t : Term L α
s : Set α
h : ↑(varFinset t) ⊆ s
v : α → M
⊢ realize (v ∘ Subtype.val) (restrictVar t (Set.inclusion h)) = realize v t
induction' t with _ _ _ _ ih
no goals
case var
L : Language
L' : Language
M : Type w
N : Type ?u.9538
P : Type ?u.9541
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
inst✝ : DecidableEq α
t : Term L α
s : Set α
h✝ : ↑(varFinset t) ⊆ s
v : α → M
_a✝ : α
h : ↑(varFinset (var _a✝)) ⊆ s
⊢ realize (v ∘ Subtype.val) (restrictVar (var _a✝) (Set.inclusion h)) = realize v (var _a✝)
rfl
case func
L : Language
L' : Language
M : Type w
N : Type ?u.9538
P : Type ?u.9541
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
inst✝ : DecidableEq α
t : Term L α
s : Set α
h✝¹ : ↑(varFinset t) ⊆ s
v : α → M
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L α
ih :
  ∀ (a : Fin l✝) (h : ↑(varFinset (_ts✝ a)) ⊆ s),
    realize (v ∘ Subtype.val) (restrictVar (_ts✝ a) (Set.inclusion h)) = realize v (_ts✝ a)
h✝ : ↑(Finset.biUnion Finset.univ fun i => varFinset (_ts✝ i)) ⊆ s
h : ∀ (i : Fin l✝), i ∈ ↑Finset.univ → ↑(varFinset (_ts✝ i)) ⊆ s
⊢ realize (v ∘ Subtype.val) (restrictVar (func _f✝ _ts✝) (Set.inclusion h✝)) = realize v (func _f✝ _ts✝)
case func
L : Language
L' : Language
M : Type w
N : Type ?u.9538
P : Type ?u.9541
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
inst✝ : DecidableEq α
t : Term L α
s : Set α
h✝ : ↑(varFinset t) ⊆ s
v : α → M
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L α
ih :
  ∀ (a : Fin l✝) (h : ↑(varFinset (_ts✝ a)) ⊆ s),
    realize (v ∘ Subtype.val) (restrictVar (_ts✝ a) (Set.inclusion h)) = realize v (_ts✝ a)
h : ↑(varFinset (func _f✝ _ts✝)) ⊆ s
⊢ realize (v ∘ Subtype.val) (restrictVar (func _f✝ _ts✝) (Set.inclusion h)) = realize v (func _f✝ _ts✝)
simp_rw [varFinset, Finset.coe_biUnion, Set.iUnion_subset_iff] at h
no goals
case func
L : Language
L' : Language
M : Type w
N : Type ?u.9538
P : Type ?u.9541
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
inst✝ : DecidableEq α
t : Term L α
s : Set α
h✝¹ : ↑(varFinset t) ⊆ s
v : α → M
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L α
ih :
  ∀ (a : Fin l✝) (h : ↑(varFinset (_ts✝ a)) ⊆ s),
    realize (v ∘ Subtype.val) (restrictVar (_ts✝ a) (Set.inclusion h)) = realize v (_ts✝ a)
h✝ : ↑(Finset.biUnion Finset.univ fun i => varFinset (_ts✝ i)) ⊆ s
h : ∀ (i : Fin l✝), i ∈ ↑Finset.univ → ↑(varFinset (_ts✝ i)) ⊆ s
⊢ realize (v ∘ Subtype.val) (restrictVar (func _f✝ _ts✝) (Set.inclusion h✝)) = realize v (func _f✝ _ts✝)
exact congr rfl (funext fun i => ih i (h i (Finset.mem_univ i)))