| Rank | Theorem | Name |
| 4 | Thm*  s:(T+T) List. paren(T;s)   no_repeats(T+T;s) (s1,s2,s3:(T+T) List, x:T. s = (s1 @ [inl(x)] @ s2 @ [inr(x)] @ s3) paren(T;s2)) | [paren_interval] |
| cites |
| 1 | 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] |
| 3 | Thm* s':(T+T) List. paren(T;s') (i:T. (inr(i)  s') (inl(i) s')) | [paren_balance2] |
| 2 | Thm* l1,l2:T List. no_repeats(T;l1 @ l2)  l_disjoint(T;l1;l2) & no_repeats(T;l1) & no_repeats(T;l2) | [no_repeats_append_iff] |
| 0 | Thm* l:T List. (l @ nil) ~ l | [append_nil_sq] |
| 0 | Thm* as,bs:T List. ||as @ bs|| = ||as||+||bs||  | [length_append] |