| | Some definitions of interest. |
|
| list-list-connect | Def L1-G- > *L2 == ( x L2.L1-G- > *x) |
|
| gr_v | Def Vertices(t) == 1of(t) |
| | | Thm* t:Graph. Vertices(t) Type |
|
| graph | Def Graph == v:Type e:Type(e  vv)Top |
| | | Thm* Graph Type{i'} |
|
| iseg | Def l1  l2 ==  l:T List. l2 = (l1 @ l) |
| | | Thm* T:Type, l1,l2:T List. l1 l2 Prop |
|
| l_all | Def (xL.P(x)) == x:T. (x L)   P(x) |
| | | Thm* T:Type, L:T List, P:(TProp). (xL.P(x)) Prop |
|
| l_exists | Def (xL.P(x)) == x:T. (x L) & P(x) |
| | | Thm* T:Type, L:T List, P:(TProp). (xL.P(x)) Prop |
|
| l_member | Def (x l) == i: . i < ||l|| & x = l[i] T |
| | | Thm* T:Type, x:T, l:T List. (x l) Prop |
