full sequent assignment Sections ClassicalProps(jlc) Doc

Def xL.P(x) == (letrec list_exists L = (Case of L; nil False ; h.t P(h) list_exists(t)) ) (L)

In prior sections: list 3 jlc sequent rank