Currently \vassign is treated like \tassign, and that is incorrect. In \tassign{a}{b}, both a and b are symbol names; from the source and the target theory.
In \vassign{a}{e} is a mathematical object (from the target theory), so e should not be checked (it can essentially be anything), or at least be checked as $e$ would be.
Currently
\vassignis treated like\tassign, and that is incorrect. In\tassign{a}{b}, bothaandbare symbol names; from the source and the target theory. In\vassign{a}{e}is a mathematical object (from the target theory), soeshould not be checked (it can essentially be anything), or at least be checked as $e$ would be.This is also one of the top-error-producing bugs.