Liouville form of an element relative to a subset

Let $G$ be a differential field with derivation $D$ and let $S\subseteq G$ be a subset. An element $h\in G$ has Liouville form in $S$ if there exist an integer $n\ge 0$, constants $c_1,\dots,c_n\in\operatorname{Con}(G)$, nonzero elements $u_1,\dots,u_n\in S$ and an element $v\in S$ such that

For $n=0$ the sum is empty and the condition reads $h=Dv$. This is the shape of the conclusion of Liouville's theorem on elementary antiderivatives; the predicate packages it so that the one-step descent lemmas of the inductive proof (from an intermediate field of a tower to the next smaller one) can be stated without repeating the existential quantifiers.

Formalization Note The constants $c_i$ range over all of $\operatorname{Con}(G)$, not over the constants of a smaller field; the descent lemmas assume $\operatorname{Con}(G)\subseteq K$ for the field $K$ they descend to.