  For the lambda-calculus with surjective pairing and terminal type, Curien and
Di Cosmo were inspired by Knuth-Bendix completion, and introduced a confluent
rewriting system that (1) extends the naive rewriting system, and (2) is stable
under contexts. The rewriting system has (i) a rule that rewrites term of a
terminal type rewrites to a term constant *, unless the term is not *, (ii)
rewrite rules for the extensionality of function types and product types, and
rewrite rules mediating the rewrite rules (i) and (ii). Curien and Di Cosmo
supposed that because of (iii), any reducibility method cannot prove the strong
normalization (SN) of Curien-Di Cosmo's rewriting system, and they left the SN
open. By relativizing Girard's reducibility method to the *-free terms, we
prove SN of their rewriting, and SN of the extension by polymorphism.
  The relativization works because: for any SN term t, and for any variable z
of terminal type not occurring in $t$, t with all the occurrences of * of
terminal type replaced by the variable z is SN.
