proposition: Lemma Equal_mapsto_iff : forall m1 m2 : farray, Equal m1 m2 <-> (m1.(default) = m2.(default) /\ forall k e, MapsTo k e m1 <-> MapsTo k e m2).
proof: Proof. intros m1 m2. split. intros Heq. unfold Equal in Heq. destruct Heq as (Hd, Heq). split; auto. intros k e. rewrite 2 find_mapsto_iff, Heq. split; auto. intros (Hd, Hiff). unfold Equal. split; auto. intro k. rewrite eq_option_alt. intro e. rewrite <- 2 find_mapsto_iff; auto. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance