F:(A
Prop), L:A List. (k:A. Dec(F(k))) 
Dec((
k
L.F(k)))P:(TProp). (xnil.P(x)) 
FalseP:(TProp), x:T, L:T List. (y[x / L].P(y)) P(x) 
(yL.P(y))| Rank | Theorem | Name |
| 3 | F:(AProp), L:A List. (k:A. Dec(F(k))) Dec((kL.F(k))) | [decidable__l_exists] |
| cites the following: | ||
| 1 | P:(TProp). (xnil.P(x)) False | [l_exists_nil] |
| 2 | P:(TProp), x:T, L:T List. (y[x / L].P(y)) P(x) (yL.P(y)) | [l_exists_cons] |