x
L.P(x) == (letrec exists L = (Case of L; nil 
false ; h.t P(h) 
exists(t)) ) (L) q == if p true else q fi
is mentioned by
| Def xL.P(x) == (letrec exists L = (Case of L; nil false ; h.t P(h) exists(t)) ) (L) | [list_exists_2] |
In prior sections: bool 1