l:T List, x:T. (x 
l) 
(
l1,l2:T List. l = (l1 @ [x] @ l2))x:T. (x nil) Falsel: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 | l:T List, x:T. (x l) (l1,l2:T List. l = (l1 @ [x] @ l2)) | [l_member_decomp] |
| cites the following: | ||
| 0 | x:T. (x nil) False | [nil_member] |
| 1 | l:T List, a,x:T. (x [a / l]) x = a (x l) | [cons_member] |
| 2 | x:T, l1,l2:T List. (x l1 @ l2) (x l1) (x l2) | [member_append] |