P:(T
Prop). (x:T. Dec(P(x))) 
(L:T List. 
x
L.(P(x)) 
xL.P(x)) Dec(Q) ((P & Q) P 
Q)| Theorem | Name | ||
| Thm* P:(TProp). (x:T. Dec(P(x))) (L:T List. xL.(P(x)) xL.P(x)) | [not_list_all_not_iff_list_exists] | ||
| cites | |||
| Thm* Dec(P) Dec(Q) ((P & Q) P Q) | [demorgan2] |