IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hevery conj
'a:S.
all
(
Q:'a 
hbool. all
(Q:'a hbool. (P:'a hbool. all
(Q:'a hbool. (P:'a hbool. (l:hlist('a). equal
(Q:'a hbool. (P:'a hbool. (l:hlist('a). (every
(Q:'a hbool. (P:'a hbool. (l:hlist('a). (((x:'a. and(P(x),Q(x)))
(Q:'a hbool. (P:'a hbool. (l:hlist('a). (,l)
(Q:'a hbool. (P:'a hbool. (l:hlist('a). ,and
(Q:'a hbool. (P:'a hbool. (l:hlist('a). ,(every(P,l)
(Q:'a hbool. (P:'a hbool. (l:hlist('a). ,,every(Q,l))))))
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
