proposition: Lemma elements_3w: forall s, NoDupA E.eq (elements s).
proof: Proof. intro. apply SortA_NoDupA with E.lt. - constructor. + intro. apply E.eq_refl. + intro. apply E.eq_sym. + intro. apply E.eq_trans. - constructor. + intros x H. apply E.lt_not_eq in H. apply H. reflexivity. + intro. apply E.lt_trans. - solve_proper. - apply elements_3. Qed.
imports: Bool PeanoNat BinPos OrderedType OrderedTypeEx FSetInterface