initial work on compiling the Vsub operation

(proofs not updated)