We are interested in verifying dynamic properties of reactive systems. The reactive systems are specified by B event systems in a refinement development. The refinement allows us to combine proof and model-checking verification techniques in a novel way. Most of the PLTL dynamic properties are preserved by refinement, but in our approach, the user can also express how a property evolves during the refinement. The preservation of the abstract property, expressed by a PLTL formula F ₁, is used as an assumption for proving a PLTL formula F ₂ which expresses an enriched property in the refined system. Formula F ₁ is verified by model-checking on the abstract system. So, to verify the enriched formula F ₂, it is enough to prove some propositions depending on the respective patterns followed by F ₁ and F ₂. In this paper, we show how to obtain these sufficient propositions from the refinement relation and the semantics of the PLTL formulae. The main advantage is that the user does not need to express a variant or a loop invariant to obtain automatic proofs of dynamic properties, at least for finite state event systems. Another advantage is that the model-checking is done on an abstraction with few states.