{α : Type u} →
  [inst : LE α] →
    {motive : OrderBot α → Sort u_1} →
      ([toBot : Bot α] → (bot_le : ∀ (a : α), ⊥ ≤ a) → motive { toBot := toBot, bot_le := bot_le }) →
        (t : OrderBot α) → motive t