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] Andre Platzer. A complete uniform substitution calculus for differential dynamic logic.  Journal of Automated Reasoning, 59(2), pp. 219-265, 2017. DOI 10.1007/s10817-016-9385-1

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