PrintForm Definitions Lemmas hol list 2 Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: every conj 2
  'a:S, Q,P:('a), l:'a List.
  every(x:'a. (P(x))(Q(x));l) = (every(P;l)every(Q;l))
By: RewriteOfThm Thm: hevery conj (SimpsetC [`hol_to_nuprl`])

Generated subgoals:

None

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

PrintForm Definitions Lemmas hol list 2 Sections HOLlib Doc