proposition: Lemma elements_spec2' : forall s acc `{Ok s}, sort X.lt acc -> (forall x y : elt, InA X.eq x acc -> InT y s -> X.lt y x) -> sort X.lt (elements_aux acc s).
proof: Proof. induction s as [ | c l Hl y r Hr]; simpl; intuition. inv. apply Hl; auto. - constructor. + apply Hr; auto. + eapply InA_InfA; eauto with *. intros. destruct (elements_spec1' r acc y0); intuition. - intros. inversion_clear H. + order. + destruct (elements_spec1' r acc x); intuition eauto. Qed.
imports: Orders OrdersFacts MSetInterface PeanoNat