proposition: Lemma Equivb_elements : forall s s', Equivb s s' <-> L.Equivb cmp (elements s) (elements s').
proof: Proof. unfold Equivb, L.Equivb; split; split; intros. - do 2 rewrite elements_in; firstorder. - destruct H. apply (H2 k); rewrite <- elements_mapsto; auto. - do 2 rewrite <- elements_in; firstorder. - destruct H. apply (H2 k); unfold L.PX.MapsTo; rewrite elements_mapsto; auto. Qed.
imports: FunInd FMapInterface FMapList ZArith Int