fact: Definition fold_left {A B:Type} (f:B->A->B): forall (b:B) {n} (v:t A n), B := fix fold_left_fix (b:B) {n} (v : t A n) : B := match v with | [] => b | a :: w => (fold_left_fix (f b a) w) end.
imports: Arith_base