Enclosed is a proof of strong normalization (SN) for simply-typed lambda-calculus (STLC) in Coq using de Bruijn indices. It uses the Tait-Girard technique of a "Reducibility" predicate which is recursive on the type. I believe it to be the smallest direct proof of that fact using those methods (i.e. de Bruijn indices in Coq), although the one by Adam Koprowski, part of the CoLoR library, is elegant and more general. See sn.pdf for more description, or start reading the Coq code at sn3.v.
tnrn9b/sn-stlc-de-bruijn-coq
Strong Normalization for Simply-Typed Lambda-Calculus with de Bruijn indices in Coq
Coq