E:(
Prop).
(EquivRel x,y:. x E y) & (x,y:. Dec(x E y)) 
(
h:(). (n,k:. (n E k) 
h(n) = h(k)) & (n:. n E (h(n))))
comp_choice
P
Thm* E:(Prop).
(EquivRel x,y:. x E y) & (x,y:. Dec(x E y))
(h:(). (n,k:. (n E k) h(n) = h(k)) & (n:. n E (h(n))))
comp_choice
Thm* R:(TTProp).
(x,y:T. Dec(x R y)) (r:(TT
). x,y:T. (x r y) (x R y))
decide_imp_bool