{α : Type u_6} →
  [inst : LE α] →
    {motive : NonemptyInterval α → Sort u} →
      ((toProd : α × α) → (fst_le_snd : toProd.1 ≤ toProd.2) → motive { toProd := toProd, fst_le_snd := fst_le_snd }) →
        (t : NonemptyInterval α) → motive t