{α : Type u_2} →
  [inst : Zero α] →
    [inst_1 : One α] →
      [inst_2 : LE α] →
        {motive : ZeroLEOneClass α → Sort u} → ((zero_le_one : 0 ≤ 1) → motive ⋯) → (t : ZeroLEOneClass α) → motive t