E:(T
TProp).
Thm* (EquivRel x,y:T. E(x,y))
Thm*
Thm* (
x,y:T. Dec(E(x,y))) (u,v:x,y:T//E(x,y). Dec(u = v))E:(TTProp).
Thm* (
x,y:T. Dec(E(x,y))) 
(
f:(TT
). x,y:T. (x f y) E(x,y))a,b:. (a b) a = b| Theorem | Name |
| E:(TTProp).
Thm* (EquivRel x,y:T. E(x,y)) Thm*
Thm* ( x,y:T. Dec(E(x,y))) (u,v:x,y:T//E(x,y). Dec(u = v)) | [decidable__quotient_equal] |
| 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] |
| a,b:. (a b) a = b | [iff_imp_equal_bool] |