∀ (X : Type u) [isSemilatticeSup : SemilatticeSup X] [isOrderBot : OrderBot X],
  sizeOf { X := X, isSemilatticeSup := isSemilatticeSup, isOrderBot := isOrderBot } =
    1 + sizeOf X + sizeOf isSemilatticeSup + sizeOf isOrderBot