graph
1
2
Sections
Graphs
Doc
Theorem
Name
Thm*
T:Type, s:(T+T) List. paren(T;s)
Prop
[paren_wf]
cites
Thm*
as,bs:T List. ||as @ bs|| = ||as||+||bs||
[length_append]
graph
1
2
Sections
Graphs
Doc
T:Type, s:(T+T) List. paren(T;s) 
Propas,bs:T List. ||as @ bs|| = ||as||+||bs|| 
T:Type, s:(T+T) List. paren(T;s) Propas,bs:T List. ||as @ bs|| = ||as||+||bs||