Sort u_1 →
  {R : Type u} →
    {L : Type v} →
      {L' : Type w} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : LieAlgebra R L] →
              [inst_3 : LieRing L'] →
                [inst_4 : LieAlgebra R L'] →
                  (L ≃ₗ⁅R⁆ L') →
                    {R' : Type u} →
                      {L' : Type v} →
                        {L'' : Type w} →
                          [inst' : CommRing R'] →
                            [inst'_1 : LieRing L'] →
                              [inst'_2 : LieAlgebra R' L'] →
                                [inst'_3 : LieRing L''] → [inst'_4 : LieAlgebra R' L''] → (L' ≃ₗ⁅R'⁆ L'') → Sort u_1