Def let x = a in b(x) == (x.b(x))(a)

Thm* a:A, b:(AB). let x = a in b(x) B