Thm* f:(TProp). (t:T. Dec(f(t))) (g:(T). t:T. f(t) g(t)) decid_is_comp

Thm* Fin(T) (m:. m ~ T) fin_iff_1_1_nsub

In prior sections: core fun 1 well fnd int 1 bool 1 int 2 list 1