Cannot define `Let-in` as derived form in dependently-typed lang

Typing Rules

We may have the expression 饾懃:=饾憽:饾憞 well-typed without having ((位饾懃:饾憞. 饾憿) 饾憽) well-typed (where 饾憞 is a type of 饾憽). This is because the value 饾憽 associated with 饾懃 may be used in a conversion rule (see Section Conversion rules).

The issue is that a well-typed expression x:=t:T does not necessarily mean that ((位x:T. u) t) is well-typed. The value t associated with x may be used in a conversion rule.