[ new ] HSubst for STLC + sums with ETA FOR SUMS!

* So, we have a *proven terminating* normalizer for STLC with
  sums which also happens to apply commuting coercions. All of
  this is implemented using Hereditary Substitution.

* This is inspired by the amazing paper
  Short Proofs of Normalization by Joachimsku and Matthes (1999)
  which introduces hereditary substitution for STLC has a proof
  method and shows how one can extract a total program from the
  proof based on Ulrich Berger's technique showcased in Program
  Extraction from Normalization.

* The implementation itself is made possible by using Conor's
  variable dropping operator, and the approach described in
  Altenkirch & Keller (2010): there is some careful inlining
  in `appNf`'s definition (e.g. Cs composition is not defined
  even if it'd be nicer to have it as a separate function)...