'a:S, l:'a List, P:('a). every(P;l)  (n:. n<||l||  P(l[n]))

By:

RewriteOfThm Thm* 'a:S.  Thm* all Thm* (l:hlist('a). all Thm* (l:hlist('a). (P:'a  hbool. equal Thm* (l:hlist('a). (P:'a  hbool. (every(P,l) Thm* (l:hlist('a). (P:'a  hbool. ,all Thm* (l:hlist('a). (P:'a  hbool. ,(n:hnum. implies Thm* (l:hlist('a). (P:'a  hbool. ,(n:hnum. (lt(n,length(l)) Thm* (l:hlist('a). (P:'a  hbool. ,(n:hnum. ,P(el(n,l))))))) (WOSimpC (ioid !oid{hel simp update:s}) (SimpsetC [`hol_to_nuprl`;`bequal`])) THEN Try (Complete Auto)

1

1. 'a:S, l:hlist('a), P:('a). every(P;l)  (n:hnum. n<||l||  P(el(n,l)))   'a:S, l:'a List, P:('a). every(P;l)  (n:. n<||l||  P(l[n]))

1 step

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html