proposition: Lemma elements_aux_mapsto : forall (s:t elt) acc x e, InA eqke (x,e) (elements_aux acc s) <-> MapsTo x e s \/ InA eqke (x,e) acc.
proof: Proof. induction s as [ | l Hl x e r Hr h ]; simpl; auto. - intuition. inversion H0. - intros. rewrite Hl. destruct (Hr acc x0 e0); clear Hl Hr. intuition; inversion_clear H3; intuition auto with ordered_type. destruct H0; simpl in *; subst; intuition. Qed.
imports: FunInd FMapInterface FMapList ZArith Int