∀ {F : Type u_1} {K : Type u_2} [inst : Field F] [inst_1 : Field K] [inst_2 : Differential F] [inst_3 : Differential K]
  [inst_4 : Algebra F K],
  (∀ (a : F) (ι : Type) [inst_5 : Fintype ι] (c : ι → F),
      (∀ (x : ι), (c x)′ = 0) →
        ∀ (u : ι → K) (v : K),
          ↑a = ∑ x, ↑(c x) * Differential.logDeriv (u x) + v′ →
            ∃ ι₀ x c₀, ∃ (_ : ∀ (x : ι₀), (c₀ x)′ = 0), ∃ u₀ v₀, a = ∑ x, c₀ x * Differential.logDeriv (u₀ x) + v₀′) →
    IsLiouville F K