∀ {α : Type u_3} {β : Type u_4} [inst : SizeOf α] [inst_1 : SizeOf β] (vertexSet : Set α) (IsLink : β → α → α → Prop)
  (edgeSet : Set β) (isLink_symm : ∀ ⦃e : β⦄, e ∈ edgeSet → Symmetric (IsLink e))
  (eq_or_eq_of_isLink_of_isLink : ∀ ⦃e : β⦄ ⦃x y v w : α⦄, IsLink e x y → IsLink e v w → x = v ∨ x = w)
  (edge_mem_iff_exists_isLink :
    autoParam (∀ (e : β), e ∈ edgeSet ↔ ∃ x y, IsLink e x y) Graph.edge_mem_iff_exists_isLink._autoParam)
  (left_mem_of_isLink : ∀ ⦃e : β⦄ ⦃x y : α⦄, IsLink e x y → x ∈ vertexSet),
  sizeOf
      { vertexSet := vertexSet, IsLink := IsLink, edgeSet := edgeSet, isLink_symm := isLink_symm,
        eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink,
        edge_mem_iff_exists_isLink := edge_mem_iff_exists_isLink, left_mem_of_isLink := left_mem_of_isLink } =
    1