val vector_update_subrange = {
  ocaml: "update_subrange",
  lem: "update_subrange_vec_dec",
  c: "vector_update_subrange",
  coq: "update_subrange_vec_dec"
} : forall 'n 'm 'o. (#\hyperref[zbits]{bits}#('n), atom('m), atom('o), #\hyperref[zbits]{bits}#('m - ('o - 1))) -> #\hyperref[zbits]{bits}#('n)