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