Nuprl - hol_list_2 LEMMAs for every_conj

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

Theorem	Name
Thm* 'a:S, Q,P:('a), l:'a List. Thm* every(x:'a. (P(x))(Q(x));l) = (every(P;l)every(Q;l))	[every_conj_2]
cites the following:
Thm* 'a:S. Thm* all Thm* (Q:'a hbool. all Thm* (Q:'a hbool. (P:'a hbool. all Thm* (Q:'a hbool. (P:'a hbool. (l:hlist('a). equal Thm* (Q:'a hbool. (P:'a hbool. (l:hlist('a). (every Thm* (Q:'a hbool. (P:'a hbool. (l:hlist('a). (((x:'a. and(P(x),Q(x))) Thm* (Q:'a hbool. (P:'a hbool. (l:hlist('a). (,l) Thm* (Q:'a hbool. (P:'a hbool. (l:hlist('a). ,and Thm* (Q:'a hbool. (P:'a hbool. (l:hlist('a). ,(every(P,l) Thm* (Q:'a hbool. (P:'a hbool. (l:hlist('a). ,,every(Q,l))))))	[hevery_conj]

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