IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
list iso1 1. 'a : S
2. r : ('a) abs_list(r) = (@a:'a List. (r = rep_list(a) ('a)))
By:
Unab [`habs_list`] THEN HN THEN Simp THEN StrongAuto
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
'a)
abs_list(r) = (@a:'a List. (r = rep_list(a) 
(
