IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
every wf12 1. 'a : Type
2. p : 'a 3. 'a List
4. u : 'a 5. v : 'a List
6. every(p;v) every(p;cons(u; v))
By:
RecUnfold `every` 0 THEN Reduce 0 THEN Simp
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html