Descent of Liouville form through an algebraic step

Let $G$ be a field of characteristic zero with a derivation $D$, let $F\subseteq G$ be a subfield, and let $K$ be an intermediate field with $D(K)\subseteq K$ and $\operatorname{Con}(G)\subseteq K$. Let $t\in G$ be algebraic over $K$ and put $L=K(t)$. Let $h\in K$. If $h$ has Liouville form in $L$, that is,

then $h$ has Liouville form in $K$ (with the same kind of data $c_j\in\operatorname{Con}(G)$, $u_j\in K^{\times}$, $v\in K$).

This is the algebraic case of the descent step in the standard induction proving Liouville's theorem on elementary antiderivatives. Mathlib contains the corresponding statement for finite-dimensional extensions of differential fields as isLiouville_of_finiteDimensional.

Formalization Note Here $G$ is only assumed to carry a derivation and to have characteristic zero; the hypotheses hK, hconst and hh state $D(K)\subseteq K$, $\operatorname{Con}(G)\subseteq K$ and $h\in K$.