P:(A
Prop). (x:A. Dec(P(x))) 
(
f:(A
). x:A. P(x) 
f(x))Q:(ABProp). (x:A. y:B. Q(x,y)) (f:(AB). x:A. Q(x,f(x))) (b:. P b)| Theorem | Name |
| P:(AProp). (x:A. Dec(P(x))) (f:(A). x:A. P(x) f(x)) | [sfa_doc_bool_vs_decidable_fun] |
| cites the following: | |
| Q:(ABProp). (x:A. y:B. Q(x,y)) (f:(AB). x:A. Q(x,f(x))) | [ax_choice] |
| (b:. P b) | [sfa_doc_bool_vs_decidable] |