zeta-reduction

(let ?var ?val ?body) => ?body[?var => ?val]

$$\frac{\mathcal{W}\mathcal{F}(E)[\Gamma ]E[\Gamma ]⊢u:UE[\Gamma ::(x:=u:U)]⊢t:T}{E[\Gamma ]⊢\mathtt{let}x:=u:U\mathtt{in}t{⊳}_{\zeta }t\{x/u\}}$$

参考文献

• Conversion rules — Coq 8.16.1 documentation