graph
1
2
Sections
Graphs
Doc
Theorem
Name
Thm*
s',s3:(T+T) List. paren(T;s')
paren(T;s3)
paren(T;s3 @ s')
[append_paren]
cites
Thm*
as:T List. (as @ nil) = as
[append_back_nil]
graph
1
2
Sections
Graphs
Doc
s',s3:(T+T) List. paren(T;s') 
paren(T;s3) paren(T;s3 @ s')as:T List. (as @ nil) = ass',s3:(T+T) List. paren(T;s') paren(T;s3) paren(T;s3 @ s')as:T List. (as @ nil) = as