proposition: Lemma elements_spec1' : forall s acc x, InA X.eq x (elements_aux acc s) <-> InT x s \/ InA X.eq x acc.
proof: Proof. induction s as [ | c l Hl x r Hr ]; simpl; auto. - intuition. inversion H0. - intros. rewrite Hl. destruct (Hr acc x0); clear Hl Hr. intuition; inversion_clear H3; intuition. Qed.
imports: Orders OrdersFacts MSetInterface PeanoNat