  Language-integrated query is a powerful programming construct allowing
database queries and ordinary program code to interoperate seamlessly and
safely. Language-integrated query techniques rely on classical results about
the nested relational calculus, stating that its queries can be algorithmically
translated to SQL, as long as their result type is a flat relation. Cooper and
others advocated higher-order nested relational calculi as a basis for
language-integrated queries in functional languages such as Links and F#.
However, the translation of higher-order relational queries to SQL relies on a
rewrite system for which no strong normalization proof has been published: a
previous proof attempt does not deal correctly with rewrite rules that
duplicate subterms. This paper fills the gap in the literature, explaining the
difficulty with a previous proof attempt, and showing how to extend the
$\top\top$-lifting approach of Lindley and Stark to accommodate duplicating
rewrites. We also show how to extend the proof to a recently-introduced
calculus for heterogeneous queries mixing set and multiset semantics.
