Completeness of a Branching-Time Logic with Possible Choices