Yes, that is the case. For checking whether a structure satisfies a property, we need to make sure that ALL initial states satisfy the property. However, the proof trees of the initial states may have significant overlaps, but we need one proof tree per initial state.