∀ {α : Type u_1} {σ : Type u_2} [inst : SizeOf α] [inst_1 : SizeOf σ] (f : σ → Set α) (top : α → σ)
  (top_mem : ∀ (x : α), x ∈ f (top x)) (inter : (a b : σ) → (x : α) → x ∈ f a ∩ f b → σ)
  (inter_mem : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), x ∈ f (inter a b x h))
  (inter_sub : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), f (inter a b x h) ⊆ f a ∩ f b),
  sizeOf { f := f, top := top, top_mem := top_mem, inter := inter, inter_mem := inter_mem, inter_sub := inter_sub } = 1