∀ {L : FirstOrder.Language} {M : Type u_4} {N : Type u_3} [inst : L.Structure M] [inst_1 : L.Structure N]
  {f : L.Hom M N},
  Function.Surjective ⇑f →
    ∀ (S : L.Substructure N),
      ∀ x ∈ S, x ∈ FirstOrder.Language.Substructure.map f (FirstOrder.Language.Substructure.comap f S)