∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (toLHom : L →ᴸ L') (invLHom : L' →ᴸ L)
  (left_inv : invLHom.comp toLHom = FirstOrder.Language.LHom.id L)
  (right_inv : toLHom.comp invLHom = FirstOrder.Language.LHom.id L') (toLHom_1 : L →ᴸ L') (invLHom_1 : L' →ᴸ L)
  (left_inv_1 : invLHom_1.comp toLHom_1 = FirstOrder.Language.LHom.id L)
  (right_inv_1 : toLHom_1.comp invLHom_1 = FirstOrder.Language.LHom.id L'),
  ({ toLHom := toLHom, invLHom := invLHom, left_inv := left_inv, right_inv := right_inv } =
      { toLHom := toLHom_1, invLHom := invLHom_1, left_inv := left_inv_1, right_inv := right_inv_1 }) =
    (toLHom = toLHom_1 ∧ invLHom = invLHom_1)