proposition: Lemma elements_spec1 : forall s x, InA X.eq x (elements s) <-> InT x s.
proof: Proof. intros; generalize (elements_spec1' s nil x); intuition. inversion_clear H0. Qed.
imports: Orders OrdersFacts MSetInterface PeanoNat