Propagation of singularities for subelliptic wave equations

We revisit the paper [Mel86] by R. Melrose, providing a full proof of the main theorem on propagation of singularities for subelliptic wave equations, and linking this result with sub-Riemannian geometry. This result asserts that singularities of subelliptic wave equations only propagate along null-bicharacteristics and abnormal extremal lifts of singular curve. As a new consequence, for x = y and denoting by K G the wave kernel, we obtain that the singular support of the distribution t $rightarrow$ K G (t, x, y) is included in the set of lengths of the normal geodesics joining x and y, at least up to the time equal to the minimal length of a singular curve joining x and y.