(assert (let (_ bv0 1)