Here you can find my TFP 2018 submission "Shifting and Resetting in the Calculus of Constructions", and a technical appendix containing elided proofs.