module Control.Fold
import Data.Vect
dfoldl : {b : Nat -> Type} -> ((m : Nat) -> b m -> a -> b (S m)) -> b Z -> Vect n a -> b n
dfoldl f z [] = z
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