IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
assert of null is mt 'a:Type, l:'a List. null(l) mt(l)
By:
Id THEN StrongAuto THEN Try (Complete (Unfold `label` 0)) THEN ListInd 2
THEN
StrongAuto
THEN
Try (Complete (Unfold `label` 0))
THEN
Simp
THEN
StrongAuto
THEN
Try (Complete (Unfold `label` 0))
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html