Nuprl - Proof: length wf1 1

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

1. A : Type
2. l : A List

||l||

By:

ListInd 2

Generated subgoals:

1   ||nil||
1 step

2 3. u : A
4. v : A List
5. ||v||
  ||u.v||
4 steps

About:

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

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