Thm* P:(AProp). (x:A. P(x) P(x)) & (x:A. P(x)) (x:A. P(x)) (x:A. P(x)) (x:A. P(x)) not_dec_is_dec

In prior sections: core bool 1 int 2 list 1