Errata TOCL'15
Definition 4.4: While correct as stated, the notion of differential expressiveness should have limited the formula G to be in L, in which case the notion is more interesting. All proofs about differential expressiveness work in that case. Also see 

[1] André Platzer. A complete uniform substitution calculus for differential dynamic logic.  Journal of Automated Reasoning, 59(2), pp. 219-265, 2017. https://doi.org/10.1007/s10817-016-9385-1

[2] André Platzer. Uniform substitution at one fell swoop. In Pascal Fontaine, editor, CADE, volume 11716 of LNCS, pp. 425-441. Springer, 2019. https://doi.org/10.1007/978-3-030-29436-6_25