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

Thm* Fin(T) (x,y:T. Dec(x = y)) fin_is_decid

Thm* f:(TS). Fin(S) & (s:S. Dec(t:T. f(t) = s)) Fin(x,y:T//(f(x) = f(y))) inv_of_fin_is_fin

Thm* R:(STProp). (s:S. Dec(t:T. R(s,t))) (f:({s:S| t:T. R(s,t) }T). s:{s:S| t:T. R(s,t) }. R(s,f(s))) set_function

Thm* B:(TProp). Fin(T) & (t:T. Dec(B(t))) Fin({t:T| B(t) }) finite_decidable_subset

Thm* n:, T:Type, B:(TProp). (n ~ T) & (t:T. Dec(B(t))) (m:. m ~ {t:T| B(t) }) fin_dec_fin

In prior sections: core int 1 bool 1 int 2