Post #1846843

@jonmsterling I could see a sort of two-worlds claim that it's reasonable. Namely, one may believe that truly everything is either true or false, that axiom of choice holds, etc, and yet still distinguish truth from the notion of construction. But under unique choice these must be the same. One could of course *still* take the narrower choice that commutes \exists! and thus results in a proposition "there exists a unique function"