a bug about the normalization rule of logic expression

Here is a bug I found in the normalization rule of logic expression.
In the Formal Semantic Doc,the logic expression is normalized as below(take AND as example):

[Expr1 and Expr2]   
==  
let $e1 := [ Expr1 ]Effective_Boolean_Value,   
     $e2 := [ Expr2 ]Effective_Boolean_Value,   
return op:boolean-and($e1, $e2)  

In fact,the output of the rule is not consistent with Core Grammar.Because in Core,the LetExpr can only have one variable as one part.So the rule should be changed to,I think:

let $e1 := [ Expr1 ]Effective_Boolean_Value return   
     let $e2 := [ Expr2 ]Effective_Boolean_Value return  
op:boolean-and($e1, $e2)  

Am'I right?从网站得到更多信息。MSN Explorer 免费下载:http://explorer.msn.com/lccn