(R : Type u_1) →
  (A : Type u_2) →
    (L : Type u_3) →
      [inst : CommRing A] →
        [inst_1 : LieRing L] →
          [inst_2 : Module A L] →
            [inst_3 : LieRingModule L A] →
              [LieRinehartRing A L] → [inst_5 : CommRing R] → [Algebra R A] → [LieAlgebra R L] → Prop