∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (dom : L.Substructure M) (cod : L.Substructure N) (toEquiv : L.Equiv ↥dom ↥cod) (dom_1 : L.Substructure M)
  (cod_1 : L.Substructure N) (toEquiv_1 : L.Equiv ↥dom_1 ↥cod_1),
  ({ dom := dom, cod := cod, toEquiv := toEquiv } = { dom := dom_1, cod := cod_1, toEquiv := toEquiv_1 }) =
    (dom = dom_1 ∧ cod = cod_1 ∧ toEquiv ≍ toEquiv_1)