Nuprl - Proof: non neg length 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: non neg length 1

1. A : Type
2. l : A List

||l||

By:

ListInd 2

Generated subgoals:

1 ||nil||0
1 step

2 3. u : A
4. v : A List
5. ||v||0
||u.v||0
1 step

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

1	\|\|nil\|\|0	1 step
2	3. u : A 4. v : A List 5. \|\|v\|\|0 \|\|u.v\|\|0	1 step