(X : LightCondSet) →
  (motive : (i : (S : LightProfinite) × X.val.obj (Opposite.op S)) × ↑i.fst.toTop → Sort u_2) →
    (x : (i : (S : LightProfinite) × X.val.obj (Opposite.op S)) × ↑i.fst.toTop) →
      ((fst : LightProfinite) → (i : X.val.obj (Opposite.op fst)) → (s : ↑⟨fst, i⟩.fst.toTop) → motive ⟨⟨fst, i⟩, s⟩) →
        motive x