{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] →
              {motive : IsLiouville F K → Sort u} →
                (t : IsLiouville F K) →
                  ((isLiouville :
                        ∀ (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₀′) →
                      motive ⋯) →
                    motive t