proposition: Lemma xfoldi_1 : forall m v i, xfoldi m v i = fold_left (fun a p => f (fst p) (snd p) a) (xelements m i) v.
proof: Proof. set (F := fun a p => f (fst p) (snd p) a). induction m; intros; simpl; auto. destruct o. - rewrite fold_left_app; simpl. rewrite <- IHm1. rewrite <- IHm2. unfold F; simpl; reflexivity. - rewrite fold_left_app; simpl. rewrite <- IHm1. rewrite <- IHm2. reflexivity. Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface