{motive : SemilatInfCat → Sort u_1} →
  (t : SemilatInfCat) →
    ((X : Type u) →
        [isSemilatticeInf : SemilatticeInf X] →
          [isOrderTop : OrderTop X] →
            motive { X := X, isSemilatticeInf := isSemilatticeInf, isOrderTop := isOrderTop }) →
      motive t