Nuprl - Pf sublist of nil iff nil 1 1

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

At: sublist of nil iff nil 1 1

1. T: Type
2. eq: {T=}
3. L: T List

xL.x(eq) nil L = nil

By: Rewrite (HigherC is_member_unrollC THENC HigherC assert_evalC) 0

Generated subgoal:

1 xL.False L = nil

About:

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