proposition: Lemma equal_spec cmp m m' {Hm:Ok m}{Hm': Ok m'} : equal cmp m m' = true <-> Equivb cmp m m'.
proof: Proof. unfold equal. split. - intros. destruct (andb_prop _ _ H); clear H. generalize (submap_2 Hm Hm' H0). generalize (submap_2 Hm' Hm H1). firstorder. - intuition. apply andb_true_intro; split; apply submap_1; unfold Submap; firstorder. Qed.
imports: Coq(EqualitiesFacts)