theorem :: BVFUNC_1:1

canceled;