∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : LieRing L] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra]
  (S : RootPairing (↥LieSubalgebra.root) K (Module.Dual K ↥H) ↥H) (i j : ↥LieSubalgebra.root)
  (motive : S.root i - S.root j ∈ Set.range ⇑S.root → Prop) (h : S.root i - S.root j ∈ Set.range ⇑S.root),
  (∀ (idx : ↥LieSubalgebra.root) (hidx : S.root idx = S.root i - S.root j), motive ⋯) → motive h