R:(T
TProp).
(x,y:T. Dec(x R y)) 
(
r:(TT
). x,y:T. (x r y) 
(x R y))
decide_imp_bool
b == if b
True else False fi
Thm* R:(TTProp).
(x,y:T. Dec(x R y)) (r:(TT). x,y:T. (x r y) (x R y))
decide_imp_bool
Thm* E:(
), n,k:.
(EquivRel x,y:. x E y) ((n E k) Min{ x | xEn } = Min{ x | xEk })
min_el_iff
Thm* E:(), n:. (EquivRel x,y:. x E y) (n E Min{ x | xEn })
min_el_sound
Thm* E:(), n,k:.
(EquivRel x,y:. x E y) (n E k) Min{ x | xEn } = Min{ x | xEk }
min_el_unique
Thm* E:(TT), s,t:T. (EquivRel x,y:T. x E y) (s E t) E(s) = E(t)
equiv_rel_fun
In prior sections: bool 1