x,y:T. Dec(x = y)) 
(s:(T+T) List, i:T. Dec((inl(i) 
s)))x:T, l:T List. (y:T. Dec(x = y)) Dec((x l))| Rank | Theorem | Name |
| 3 | Thm* (x,y:T. Dec(x = y)) (s:(T+T) List, i:T. Dec((inl(i) s))) | [decidable__l_member_paren] |
| cites | ||
| 2 | Thm* x:T, l:T List. (y:T. Dec(x = y)) Dec((x l)) | [l_member_decidable] |