y
L.y-G- > *x)
t:Graph. Vertices(t) Type
e:Type(e
vv)Top Type{i'} l) == i:
. i < ||l|| & x = l[i] TT:Type, x:T, l:T List. (x l) Prop
A == A 
FalseA:Prop. (A) Prop| Some definitions of interest. | |
| list-connect | Def L-G- > *x == (yL.y-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_member | Def (x l) == i:. i < ||l|| & x = l[i] T |
| Thm* T:Type, x:T, l:T List. (x l) Prop | |
| not | Def A == A False |
| Thm* A:Prop. (A) Prop |
About:
 |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |