∀ {α : Type u} [inst : SizeOf α] (toCompleteLattice : CompleteLattice α)
  (inf_sSup_le_iSup_inf : ∀ (a : α) (s : Set α), a ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b)
  (iInf_sup_le_sup_sInf : ∀ (a : α) (s : Set α), ⨅ b ∈ s, a ⊔ b ≤ a ⊔ sInf s),
  sizeOf
      { toCompleteLattice := toCompleteLattice, inf_sSup_le_iSup_inf := inf_sSup_le_iSup_inf,
        iInf_sup_le_sup_sInf := iInf_sup_le_sup_sInf } =
    1 + sizeOf toCompleteLattice