∀ (X : Type u) [isSemilatticeInf : SemilatticeInf X] [isOrderTop : OrderTop X],
  sizeOf { X := X, isSemilatticeInf := isSemilatticeInf, isOrderTop := isOrderTop } =
    1 + sizeOf X + sizeOf isSemilatticeInf + sizeOf isOrderTop