map2gen.v

Inductive bvec (T : Set) : nat -> Set :=
  | BLeaf : T -> bvec T 0
  | BNode log2len : bvec T log2len -> bvec T log2len -> bvec T (S log2len).

Definition bvec_leaf T (v : bvec T 0) := let 'BLeaf a := v in a.
Definition bvec_l T n (v : bvec T (S n)) := let 'BNode n l _ := v in l.
Definition bvec_r T n (v : bvec T (S n)) := let 'BNode n _ r := v in r.

Fixpoint zip (T U V : Set) (f : T -> U -> V) n (u : bvec T n) :=
  match u in bvec _ n return bvec U n -> bvec V n with
    | BLeaf a => fun v => BLeaf (f a (bvec_leaf v))
    | BNode _ l r => fun v => BNode (zip f l (bvec_l v)) (zip f r (bvec_r v))
  end.