(
e:(A
A
). 
x,y:A. (x e y) x = y)E:(TTProp).
Thm* (
x,y:T. Dec(E(x,y))) (f:(TT). x,y:T. (x f y) E(x,y))| Theorem | Name |
| (e:(AA). x,y:A. (x e y) x = y) | [discrete_vs_bool] |
| cites the following: | |
| E:(TTProp).
Thm* ( x,y:T. Dec(E(x,y))) (f:(TT). x,y:T. (x f y) E(x,y)) | [dec_iff_ex_bvfun] |