{α : Type u_3} →
  {β : Type u_4} →
    (vertexSet : Set α) →
      (IsLink : β → α → α → Prop) →
        (edgeSet : Set β) →
          (∀ ⦃e : β⦄, e ∈ edgeSet → Symmetric (IsLink e)) →
            (∀ ⦃e : β⦄ ⦃x y v w : α⦄, IsLink e x y → IsLink e v w → x = v ∨ x = w) →
              autoParam (∀ (e : β), e ∈ edgeSet ↔ ∃ x y, IsLink e x y) Graph.edge_mem_iff_exists_isLink._autoParam →
                (∀ ⦃e : β⦄ ⦃x y : α⦄, IsLink e x y → x ∈ vertexSet) → Graph α β