fact: Definition fold_left2 {A B C: Type} (f : A -> B -> C -> A) := fix fold_left2_fix (a : A) {n} (v : t B n) : t C n -> A := match v in t _ n0 return t C n0 -> A with |[] => fun w => case0 (fun _ => A) a w |@cons _ vh vn vt => fun w => caseS' w (fun _ => A) (fun wh wt => fold_left2_fix (f a vh wh) vt wt) end.
imports: Arith_base