proposition: Lemma Equal_Equiv : forall (m m' : farray), Equal m m' <-> Equiv m m'.
proof: Proof. intros. rewrite Equal_mapsto_iff. split; intros. split. split; intros (e,Hin); exists e; unfold MapsTo in H; [rewrite <- H|rewrite H]; auto. intros; apply MapsTo_fun with m k; auto; rewrite H; auto. split; intros H'. destruct H. assert (Hin : In k m') by (rewrite <- H; exists e; auto). destruct Hin as (e',He'). rewrite (H0 k e e'); auto. destruct H. assert (Hin : In k m) by (rewrite H; exists e; auto). destruct Hin as (e',He'). rewrite <- (H0 k e' e); auto. Qed.
imports: SetoidList Bool OrderedType OrdersLists RelationPairs Orders RelationClasses