∀ {L : FirstOrder.Language} {T : L.Theory},
  T.IsComplete →
    ∀ (M : Type u_1) (N : Type u_2) [inst : L.Structure M] [inst_1 : L.Structure N] [M ⊨ T] [N ⊨ T] [Nonempty M]
      [Nonempty N], L.ElementarilyEquivalent M N