proposition: Lemma elements_aux_sort : forall (s:t elt) acc, bst s -> sort ltk acc -> (forall x e y, InA eqke (x,e) acc -> In y s -> X.lt y x) -> sort ltk (elements_aux acc s).
proof: Proof. induction s as [ | l Hl y e r Hr h]; simpl; intuition. inv bst. apply Hl; auto. - constructor. + apply Hr; eauto. + apply InA_InfA with (eqA:=eqke). * auto with typeclass_instances. * intros (y',e') H6. destruct (elements_aux_mapsto r acc y' e'); intuition. -- red; simpl; eauto. -- red; simpl; eauto with ordered_type. - intros x e0 y0 H H6. inversion_clear H. + destruct H7; simpl in *. order. + destruct (elements_aux_mapsto r acc x e0); intuition eauto with ordered_type. Qed.
imports: FunInd FMapInterface FMapList ZArith Int