Goal:
    elt : Type  eq_elt : elt -> elt -> Prop  m : t elt  m' : t elt
  ============================
   (Forall
      (fun '(k, _) =>
       match find k m with
       | Some x =>
           match find k m' with
           | Some y0 => eq_elt x y0
           | None => False
           end
       | None => match find k m' with
                 | Some _ => False
                 | None => True
                 end
       end) (elements m) /\
    Forall
      (fun '(k, _) =>
       match find k m with
       | Some x =>
           match find k m' with
           | Some y0 => eq_elt x y0
           | None => False
           end
       | None => match find k m' with
                 | Some _ => False
                 | None => True
                 end
       end) (elements m') <->
    (forall k : key,
     (exists e : elt, MapsTo k e m) <-> (exists e : elt, MapsTo k e m')) /\
    (forall (k : key) (e e' : elt),
     MapsTo k e m -> MapsTo k e' m' -> eq_elt e e'))


DEBUG:Going to execute:
<coq-core.plugins.ltac::setoid_rewrite@0> $1 $2