proposition: Lemma elements_in : forall (s:t elt) x, L.PX.In x (elements s) <-> In x s.
proof: Proof. intros. unfold L.PX.In. rewrite <- In_alt; unfold In0. firstorder. - exists x0. rewrite <- elements_mapsto; auto. - exists x0. unfold L.PX.MapsTo; rewrite elements_mapsto; auto. Qed.
imports: FunInd FMapInterface FMapList ZArith Int