At:
vertex-subset wf
For any graph
the_obj:GraphObject(the_graph), P:(V). vertex-subset(the_obj;x.P(x)) V List
By:
UnivCD
THEN
Unfold `vertex-subset` 0
THEN
Assert (the_obj.vacc ((Vertices(the_graph) List)Vertices(the_graph)(Vertices(the_graph) List))(Vertices(the_graph) List)(Vertices(the_graph) List))
Generated subgoals:
For any graph
the_obj:GraphObject(the_graph), P:(V
). vertex-subset(the_obj;x.P(x)) 
V List