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

[Consuelo_Goyette]

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).

[Adrienne_Shields33 (Adrienne Shields)]

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.