funelim of high order function using Type results in "Product do not match" error

[terencode]

originally reported on Zulip

This does not work:

Equations fold_left2  (Acc A B : Type) (f : Acc -> A -> B -> Acc) (acc:Acc) (l1 : list A) (l2 : list B) (Heq: List.length l1 = List.length l2) : Acc by struct l2 :=
| _,_,_,_, _, nil, nil,_ => acc
| _,_,_,_, acc, cons b1 t1,cons b2 t2,_ => fold_left2 _ _ _ f (f acc b1 b2) t1 t2 _
.

Goal forall n, forall l1 l2, forall (H: List.length l1 = List.length l2), fold_left2 _ _ _ (fun acc l1 l2 => acc + l1 + l2) n l1 l2 H = List.fold_left plus l2 (List.fold_left plus l1 n).
Proof.
    intros n l1 l2 H.
    funelim (fold_left2 nat nat nat _ n l1 l2 H).
Abort.

But this does:

Section f.
Context   (Acc A B : Type).
Equations fold_left2 (f : Acc -> A -> B -> Acc) (acc:Acc) (l1 : list A) (l2 : list B) (Heq: List.length l1 = List.length l2) : Acc by struct l2 :=
| _, _, nil, nil,_ => acc
| _, acc, cons b1 t1,cons b2 t2,_ => fold_left2 f (f acc b1 b2) t1 t2 _
.
End f.

Goal forall n, forall l1 l2, forall (H: List.length l1 = List.length l2), fold_left2 _ _ _ (fun acc l1 l2 => acc + l1 + l2) n l1 l2 H = List.fold_left plus l2 (List.fold_left plus l1 n).
Proof.
  intros n l1 l2 H.
  funelim (fold_left2 nat nat nat _ n l1 l2 H).
Qed.