∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N]
  (S T : L.Substructure M) (f : L.Hom M N),
  FirstOrder.Language.Substructure.map f (S ⊔ T) =
    FirstOrder.Language.Substructure.map f S ⊔ FirstOrder.Language.Substructure.map f T