IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hevery def2 1. 'a : S
2. P : 'a 3. h : 'a 4. t : 'a List
every(P;cons(h; t)) = ((P(h))every(P;t))
By:
RW (AddrC [2] (RecUnfoldC `every`)) 0 THEN Simp
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
every(P;cons(h; t)) = ((P(h))
every(P;t))
