finite sets Sections AutomataTheory Doc

Def b == if b True else False fi

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

Thm* Fin(St) (eq:(StSt). x,y:St. eq(x,y) x = y) fin_dist_func

In prior sections: bool 1 list 1