∀ {R : Type u_1} {L : Type u_2} {inst : CommRing R} {inst_1 : LieAdmissibleRing L}
  (motive : LieAdmissibleAlgebra R L → Prop) (h : LieAdmissibleAlgebra R L),
  (∀ (smul : R → L → L) (mul_smul : ∀ (x y : R) (b : L), (x * y) • b = x • y • b) (one_smul : ∀ (b : L), 1 • b = b)
      (smul_zero : ∀ (a : R), a • 0 = 0) (smul_add : ∀ (a : R) (x y : L), a • (x + y) = a • x + a • y)
      (add_smul : ∀ (r s : R) (x : L), (r + s) • x = r • x + s • x) (zero_smul : ∀ (x : L), 0 • x = 0)
      (smul_assoc : ∀ (x : R) (y z : L), (x • y) • z = x • y • z)
      (smul_comm : ∀ (m : R) (n a : L), m • n • a = n • m • a),
      motive
        { smul := smul, mul_smul := mul_smul, one_smul := one_smul, smul_zero := smul_zero, smul_add := smul_add,
          add_smul := add_smul, zero_smul := zero_smul, smul_assoc := smul_assoc, smul_comm := smul_comm }) →
    motive h