{α : Type u} →
  {motive : Shelf α → Sort u_1} →
    (t : Shelf α) →
      ((act : α → α → α) →
          (self_distrib : ∀ {x y z : α}, act x (act y z) = act (act x y) (act x z)) →
            motive { act := act, self_distrib := self_distrib }) →
        motive t