∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {s : Set M},
  (FirstOrder.Language.Substructure.closure L).toFun s = ⊤ → ∀ {f g : L.Hom M N}, Set.EqOn (⇑f) (⇑g) s → f = g