'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* 'a:S, Q,P:('a), l:'a List. Thm* every(x:'a. (P(x))(Q(x));l) = (every(P;l)every(Q;l)) (SimpsetC [`bequal`])

None

About: IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html