[isabelle] computation_check with "let ... in ..."

Dear code generation experts,

I was wondering how can we computation_check a term with the form “let … in …”. Here is a small example: given a proposition that can be proved by evalutaion (i.e., by eval or by by code_simp),

lemma "let x ::int poly= [:2,3:] in [:1,2:] * x = [:2, 7, 6:]”

I want to solve it using the computation_check mechanic. If I unfold the “let” constant first, the proposition can be proved like the following:

ML ‹
val holds = @{computation_check terms:
Trueprop
"times::int poly ⇒ _"
"HOL.equal ::int poly ⇒ _"
"0 :: int poly"
"pCons :: int ⇒ _"
"0 :: int" "1 :: int"
Code_Target_Int.positive datatypes:num
};
›

lemma "let x::int poly= [:2,3:] in [:1,2:] * x = [:2, 7, 6:]"
unfolding Let_def
apply (tactic ‹
CONVERSION (holds @{context}) 1
›)
by (rule TrueI)

However, without the unfolding (i.e., remove “unfolding Let_def”), "apply (tactic ‹CONVERSION (holds@{context}) 1›)” will get stuck. I am not sure if there is any other constant I should add to “@{computation_check terms:
...
};"
to make the CONVERSION work.