x
L2.L1-G- > *x)t:Graph. Vertices(t) Type
e:Type(e
vv)Top Type{i'}xL.P(x)) == x:T. (x L) 
P(x)T:Type, L:T List, P:(TProp). (xL.P(x)) Prop
xL.P(x)) == x:T. (x L) & P(x)T:Type, L:T List, P:(TProp). (xL.P(x)) Prop| Some definitions of interest. | |
| list-list-connect | Def L1-G- > *L2 == (xL2.L1-G- > *x) |
| gr_v | Def Vertices(t) == 1of(t) |
| Thm* t:Graph. Vertices(t) Type | |
| graph | Def Graph == v:Typee:Type(evv)Top |
| Thm* Graph Type{i'} | |
| 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 |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |
 |