eq:EqDecider(A), L:A List, x:A. deq-member(eq;x;L) 
(x 
L)l:T List, a,x:T. (x [a / l]) x = a 
(x l)| Rank | Theorem | Name |
| 2 | eq:EqDecider(A), L:A List, x:A. deq-member(eq;x;L) (x L) | [assert-deq-member] |
| cites the following: | ||
| 1 | l:T List, a,x:T. (x [a / l]) x = a (x l) | [cons_member] |