let sym_d_bv_sub = function Bv(Sub(n, i, j)) -> (n, i, j) | _ -> assert false