let_CONV : term -> thm
let v1 = t1 and ... and vn = tn in t
|- (let v1 = t1 and ... and vn = tn in t) = t[t1,...,tn/v1,...,vn]
let_CONV `let= in t`
|- (let= in t) = t[t1,...,tn/v1,...,vn]
# let_CONV `let x = 1 in x+y`;; val it : thm = |- (let x = 1 in x + y) = 1 + y
# let_CONV `let (x,y) = (1,2) in x+y`;; val it : thm = |- (let x,y = 1,2 in x + y) = 1 + 2
# let_CONV `let x = 1 and y = 2 in x + y + z`;; val it : thm = |- (let x = 1 and y = 2 in x + y + z) = 1 + 2 + z