∀ {α : Type u_8} {β : Type u_9} [inst : InfSet α] [inst_1 : InfSet β] [inst_2 : SizeOf α] [inst_3 : SizeOf β]
  (toFun : α → β) (map_sInf' : ∀ (s : Set α), toFun (sInf s) = sInf (toFun '' s)),
  sizeOf { toFun := toFun, map_sInf' := map_sInf' } = 1