is mentioned by

Thm* R1,R2:(TTProp). (x,y:T. R1(x,y) R2(x,y)) Graph(x,y:T. R1(x,y)) Graph(x,y:T. R2(x,y))	[rel-graph_functionality]
Thm* For any graph x,y:V. x-the_graph- > *y Prop	[connect_wf]
Thm* P:(((T+T) List)Prop). P(nil) (s1,s2:(T+T) List. P(s1) P(s2) paren(T;s1) paren(T;s2) P(s1 @ s2)) (s:(T+T) List, t:T. P(s) paren(T;s) P([inl(t)] @ s @ [inr(t)])) (s:(T+T) List. paren(T;s) P(s))	[paren_induction]
Thm* T:Type, s:(T+T) List. paren(T;s) Prop	[paren_wf]
Thm* r:, k:, L: List. r- > L^k Prop	[arrows_wf]

In prior sections: core well fnd int 1 bool 1 int 2 rel 1 fun 1 list 1 mb basic mb nat mb list 1 mb list 2 graph 1 1

Try larger context: Graphs