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