| Rank | Theorem | Name |
| 7 | Thm* For any graph
 the_obj:GraphObject(the_graph), P:(V   ). no_repeats(V;vertex-subset(the_obj;x.P(x))) & (x:V. (x  vertex-subset(the_obj;x.P(x)))   P(x)) | [vertex-subset-properties] |
| cites |
| 0 | Thm* For any graph
the_obj:GraphObject(the_graph). (x,y:V. the_obj.eq(x,y) x = y) & (T:Type, s:T, x:V, f:(TVT).  L:V List. (y:V. x-the_graph- > y (y L)) & the_obj.eacc(f,s,x) = list_accum(s',x'.f(s',x');s;L)) & (T:Type, s:T, f:(TVT). L:V List. no_repeats(V;L) & (y:V. (y L)) & the_obj.vacc(f,s) = list_accum(s',x'.f(s',x');s;L)) | [graphobj-properties] |
| 4 | Thm* L:T List. no_repeats(T;rev(L)) no_repeats(T;L) | [no_repeats_reverse] |
| 2 | Thm* P:(T), L:T List, x:T. (x filter(P;L)) (x L) & P(x) | [member_filter] |
| 3 | Thm* x:T, L:T List. (x rev(L)) (x L) | [member_reverse] |
| 0 | Thm* as:T List. (as @ nil) = as | [append_back_nil] |
| 1 | Thm* P:(T), L2,L1:T List. list_accum(l,x.if P(x) [x / l] else l fi;L1;L2) ~ (rev(filter(P;L2)) @ L1) | [filter_list_accum] |
| 6 | Thm* P:(T), l:T List. no_repeats(T;l)  no_repeats(T;filter(P;l)) | [no_repeats_filter] |