eq:{T
}, P:(T
), L:T List. 
x
L.P(x) 
(
x:{x:T| x(eq) L }. P(x))p,q:. (p
q) 
p & q Dec(Q) ((P & Q) P 
Q)eq:{T}, u:T. eq(u,u)P:. P P = true| Theorem | Name | ||
| Thm* eq:{T}, P:(T), L:T List. xL.P(x) (x:{x:T| x(eq) L }. P(x)) | [not_list_all_2_implies_exists_not] | ||
| cites | |||
| Thm* p,q:. (pq) p & q | [assert_of_band] | ||
| Thm* Dec(P) Dec(Q) ((P & Q) P Q) | [demorgan2] | ||
| Thm* eq:{T}, u:T. eq(u,u) | [equivalence_reflexive] | ||
| Thm* P:. P P = true | [assert_iff_btrue] |