'a:S, Q,P:('a
), l:'a List.
Thm* every(
x:'a. (P(x))
(Q(x));l) 
every(P;l) & every(Q;l)'a:S, Q,P:('a), l:'a List.
Thm* every(
x:'a. (P(x))(Q(x));l) = (every(P;l)every(Q;l))| Rank | Theorem | Name |
| 2 | '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] |
| cites the following: | ||
| 1 | '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] |