eq)(L,M) == ((
eq)(L,M))
((eq)(M,L))
x
L.P(x) == (letrec all L = (Case of L; nil 
true ; h.t P(h)(all(t))) ) (L)q == if p q else false fi
is mentioned by
| Def (~eq)(L,M) == ((eq)(L,M))((eq)(M,L)) | [list_iso_2] |
| Def xL.P(x) == (letrec all L = (Case of L; nil true ; h.t P(h)(all(t))) ) (L) | [list_all_2] |
In prior sections: bool 1