The Coq mailing list

["William J. Bowman" <wjb AT williamjbowman.com>]

McBride and McKinna observe that when you have let and δ reduction, including 
substitution is unnecesary.
(The View From The Left, https://dl.acm.org/citation.cfm?id=967496)
Instead, we can replace dependent typing rules such as:

  ...
  ------------------
  Γ ⊢ e₁ e₂ : B[e₂/x]

By

  ...
  ------------------
  Γ ⊢ e₁ e₂ : let x = e₂ in B

And replace substitution in reduction, such as β, by:

  Γ ⊢ (λ x.e) v → let x = v in e

Why does CIC include both let + δ reduction *and* substitution?

-- 
William J. Bowman
Northeastern University
College of Computer and Information Science