P:(T
ZProp). (x:T, y:Z. Dec(P(x,y))) 
(
f_p:(TZ
). x:T, y:Z. P(x,y) 
f_p(x,y))P:(TProp). (x:T. Dec(P(x))) (f_p:(T). x:T. P(x) f_p(x))x:A. B(x) == x:A
B(x)
is mentioned by
| Thm* P:(TZProp). (x:T, y:Z. Dec(P(x,y))) (f_p:(TZ). x:T, y:Z. P(x,y) f_p(x,y)) | [decidable_iff_exists_bool_function_2] |
| Thm* P:(TProp). (x:T. Dec(P(x))) (f_p:(T). x:T. P(x) f_p(x)) | [decidable_iff_exists_bool_function] |
In prior sections: core discrete jlc