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

At: sublist of nil iff nil 1 1 1 2 2

1. T: Type
2. eq: {T=}
3. L: T List
4. u: T
5. v: T List
6. u.v = nil

xv.False

By:
ApFunToHypEquands `x' if null(x) 0 else 1 fi -1
THEN
Reduce -1


Generated subgoals:

None

About:
listconsnilifthenelseintnatural_numberuniverseequalfalse

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