case var
L : Language
M : Type w
N : Type ?u.14398
P : Type ?u.14401
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
α : Type u_1
xs : α → M
h : ∀ (a : α), xs a ∈ S
a : α
⊢ realize xs (var a) ∈ S

case func
L : Language
M : Type w
N : Type ?u.14398
P : Type ?u.14401
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
α : Type u_1
xs : α → M
h : ∀ (a : α), xs a ∈ S
n : ℕ
f : Functions L n
ts : Fin n → Term L α
ih : ∀ (a : Fin n), realize xs (ts a) ∈ S
⊢ realize xs (func f ts) ∈ S
L : Language
M : Type w
N : Type ?u.14398
P : Type ?u.14401
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
α : Type u_1
t : Term L α
xs : α → M
h : ∀ (a : α), xs a ∈ S
⊢ realize xs t ∈ S
induction' t with a n f ts ih
no goals
case var
L : Language
M : Type w
N : Type ?u.14398
P : Type ?u.14401
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
α : Type u_1
xs : α → M
h : ∀ (a : α), xs a ∈ S
a : α
⊢ realize xs (var a) ∈ S
exact h a
no goals
case func
L : Language
M : Type w
N : Type ?u.14398
P : Type ?u.14401
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
α : Type u_1
xs : α → M
h : ∀ (a : α), xs a ∈ S
n : ℕ
f : Functions L n
ts : Fin n → Term L α
ih : ∀ (a : Fin n), realize xs (ts a) ∈ S
⊢ realize xs (func f ts) ∈ S
exact Substructure.fun_mem _ _ _ ih