{motive : BddDistLat → Sort u} →
  ((toDistLat : DistLat) →
      [isBoundedOrder : BoundedOrder ↑toDistLat] →
        motive { toDistLat := toDistLat, isBoundedOrder := isBoundedOrder }) →
    (t : BddDistLat) → motive t