no goals
L : Language
M : Type w
N : Type ?u.100902
P : Type u_1
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
s : Set M
S : Substructure L P
⊢ ∀ (x : P), x ∈ comap (Hom.id L P) S ↔ x ∈ S
simp