{α : Type u_3} →
  {β : Type u_4} →
    {motive : Graph α β → Sort u} →
      (t : Graph α β) →
        ((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 : ∀ (e : β), e ∈ edgeSet ↔ ∃ x y, IsLink e x y) →
                      (left_mem_of_isLink : ∀ ⦃e : β⦄ ⦃x y : α⦄, IsLink e x y → x ∈ vertexSet) →
                        motive
                          { 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 }) →
          motive t