fun memcpy {n:nat}
  {n1,n2:nat | n <= n1; n <= n2} {l:addr} (
    pf_dst: !bytes n1 @ l | p_dst: ptr l, p_src: &bytes n2, n: size_t n
  ) :<> ptr l = "atslib_memcpy"
// end of [memcpy]