IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
length of null list A:Type, as:A List. as = nil ||as|| = 0
By:
UnivCD THEN (HypSubst -1 0) THEN (AbReduce 0)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
A:Type, as:A List. as = nil 
||as|| = 0
