∀ {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled L.Structure)} {M : Type w} [inst : L.Structure M]
  {N : Type w} [inst_1 : L.Structure N] [inst_2 : Countable ((l : ℕ) × L.Functions l)] [inst_3 : Countable M]
  [inst_4 : Countable N],
  FirstOrder.Language.IsFraisseLimit K M → FirstOrder.Language.IsFraisseLimit K N → Nonempty (L.Equiv M N)