case h
L : Language
M : Type w
N : Type ?u.671067
P : Type ?u.671070
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
A s : Set M
h : A ⊆ ↑S
x✝ : M
⊢ x✝ ∈ ↑(LHom.substructureReduct (lhomWithConstants L ↑A)) (withConstants S h) ↔ x✝ ∈ S
L : Language
M : Type w
N : Type ?u.671067
P : Type ?u.671070
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
A s : Set M
h : A ⊆ ↑S
⊢ ↑(LHom.substructureReduct (lhomWithConstants L ↑A)) (withConstants S h) = S
ext
no goals
case h
L : Language
M : Type w
N : Type ?u.671067
P : Type ?u.671070
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
A s : Set M
h : A ⊆ ↑S
x✝ : M
⊢ x✝ ∈ ↑(LHom.substructureReduct (lhomWithConstants L ↑A)) (withConstants S h) ↔ x✝ ∈ S
simp