import Data.Nat

dfoldl : {b : Nat -> Type} -> ((m : Nat) -> b m -> a -> b (S m)) -> b Z -> Vect n a -> b n

dfoldl : {b : Nat -> Type} -> ((0 m : Nat) -> b m -> a -> b (S m)) -> b m -> Vect n a -> b (n + m)

dfoldl f z (x::xs) = dfoldl f' (f 0 z x) xs where
    f' : (m : Nat) -> b (S m) -> a -> b $ S $ S m
    f' m = f $ S m

dfoldl {n=S n} f z (x::xs) = rewrite plusSuccRightSucc n m in dfoldl f (f m z x) xs