assert length <| {size:nat} 'a array(size) -> int(size)
and    sub <| {size:nat, i:nat | i < size } 'a array(size) * int(i) -> 'a
and    update <| {size:nat, i:nat | i < size} 'a array(size) * int(i) * 'a -> unit

fun('a){m:nat, n:nat}
    bcopy(src, dest) =
    let
	fun loop(i, l) =
	    if i = l then ()
	    else (update(dest, i, sub(src, i)); loop(i+1, l))
        where loop <| {i: nat, l:nat | i <= l /\ l <= min(m,n)} int(i) * int(l) -> unit
    in
	if (length(src) < length(dest)) then loop(0, length(src))
	else loop(0, length(dest))
    end
where bcopy <| 'a array(m) * 'a array(n) -> unit