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
Q == (P Q) & (P Q)
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
Thm* E:(), n,k:.
(EquivRel x,y:. x E y) ((n E k) Min{ x | xEn } = Min{ x | xEk })
min_el_iff
Thm* f:(), n,k:.
f(n) = f(k) MinArg(f : {0..n
}) = MinArg(f : {0..k}) 
min_arg_iff