Fixpoint map2gen {A B C n} (f : A -> B -> C) (xs : ilist A n) : ilist B n -> ilist C n :=
  match xs in ilist _ n return ilist B n -> ilist C n with
    | INil => fun _ => INil
    | ICons n' x xs' => fun ys => ICons (f x (hd ys)) (map2gen f xs' (tl ys))
  end.