Nuprl - Pf is member wf nil 1

(2steps) PrintForm Definitions list 3 jlc Sections Support(jlc) Doc

At: is member wf nil 1

1. T: Type
2. eq: TT
3. u: T

u(eq) nil

By: Rewrite (HigherC is_member_unrollC) 0

Generated subgoals:

None

About:

(2steps) PrintForm Definitions list 3 jlc Sections Support(jlc) Doc