Definitions graph 1 2 Sections Graphs Doc

Some definitions of interest.
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'}
paren Def paren(T;s) == s = nil (T+T) List (t:T, s':(T+T) List. s = ([inl(t)] @ s' @ [inr(t)]) & paren(T;s')) (s',s'':(T+T) List. ||s'|| < ||s|| & ||s''|| < ||s|| & s = (s' @ s'') & paren(T;s') & paren(T;s'')) (recursive)
Thm* T:Type, s:(T+T) List. paren(T;s) Prop

About:
productproductlistconsnilless_thanunioninl
inrfunctionrecursive_def_noticeuniverseequal
membertoppropandorallexists
!abstraction

Definitions graph 1 2 Sections Graphs Doc