proposition: Lemma fold_spec' {A} (f : elt -> A -> A) (s : tree) (i : A) (acc : list elt) : fold_left (flip f) (elements_aux acc s) i = fold_left (flip f) acc (fold f s i).
proof: Proof. revert i acc. induction s as [|c l IHl x r IHr]; simpl; intros; auto. rewrite IHl. simpl. unfold flip at 2. apply IHr. Qed.
imports: Orders OrdersFacts MSetInterface PeanoNat