list 3 jlc Sections Support(jlc) Doc

Def filter(f;L) == (letrec filter f L = (Case of L; nil nil ; h.t if f(h) h.filter(f,t) else filter(f,t) fi) ) (f,L)

is mentioned by

Thm* eq:{T=}, P:(T), L:T List, x:T. x(eq) L P(x) x(eq) filter((x.P(x));L)[filter_is_member_lemma]
Thm* eq:{T=}, P:(T), L:T List, x:T. x(eq) filter((x.P(x));L) P(x)[is_member_filter_lemma]


list 3 jlc Sections Support(jlc) Doc