is mentioned by

Thm* A:AdjList, T:Type, s:T, f:(TVertices(adjl-graph(A))T). L:Vertices(adjl-graph(A)) List. no_repeats(Vertices(adjl-graph(A));L) & (y:Vertices(adjl-graph(A)). (y L)) & adjl-vertex-accum(A;s',x'.f(s',x');s) = list_accum(s',x'.f(s',x');s;L)	[adjl-vertex-accum-properties]
Def adjl-obj{\\\\v:l,i:l}(A) == mkgraphobj(x,y. x =A= y, ext{assert_eq_adjl}(A), f,s,x. adjl-edge-accum(A;s',x'.f(s',x');s;x), ext{adjl_DASH_edge_DASH_accum_DASH_properties}{i:l}(A), f,s. adjl-vertex-accum(A;s',x'.f(s',x');s), ext{adjl_DASH_vertex_DASH_accum_DASH_properties}{i:l}(A), )	[adjl-obj]

Try larger context: Graphs