{motive : NonemptyFinLinOrd → Sort u} →
  (t : NonemptyFinLinOrd) →
    ((toLinOrd : LinOrd) →
        [nonempty : Nonempty ↑toLinOrd] →
          [fintype : Fintype ↑toLinOrd] → motive { toLinOrd := toLinOrd, nonempty := nonempty, fintype := fintype }) →
      motive t