x:T, L:T List. (x 
rev(L)) 
(x L)l:T List, a,x:T. (x [a / l]) x = a 
(x l)x:T, l1,l2:T List. (x l1 @ l2) (x l1) (x l2)| Rank | Theorem | Name |
| 3 | Thm* x:T, L:T List. (x rev(L)) (x L) | [member_reverse] |
| cites | ||
| 1 | Thm* l:T List, a,x:T. (x [a / l]) x = a (x l) | [cons_member] |
| 2 | Thm* x:T, l1,l2:T List. (x l1 @ l2) (x l1) (x l2) | [member_append] |