x,y:T. Dec(x = y)) 
(s:T List, z:T. (z 
s) (
s1,s2:T List. s = (s1 @ [z / s2]) & 
(z s1)))l:T List, a,x:T. (x [a / l]) 
x = a 
(x l)| Rank | Theorem | Name |
| 2 | Thm* (x,y:T. Dec(x = y)) (s:T List, z:T. (z s) (s1,s2:T List. s = (s1 @ [z / s2]) & (z s1))) | [l_member_decomp2] |
| cites | ||
| 1 | Thm* l:T List, a,x:T. (x [a / l]) x = a (x l) | [cons_member] |