proposition: Lemma foldi_to_list : forall A B (f : A -> B -> A) a e, foldi (fun i x => f x (a.[i])) 0 (length a) e = fold_left f (to_list a) e.
proof: Proof. intros A B f a e; unfold to_list. rewrite <- fold_left_rev_right, rev_involutive. apply (foldi_ind2 _ _ (fun _ a b => a = fold_right (fun y x => f x y) e b)). apply leb_0. reflexivity. intros i x l _ Hi IH. simpl; f_equal; exact IH. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz