title: Odd behavior of setoid_rewrite in Coq
body: <p>I am having problems with rewriting using the <code>setoid_rewrite</code> tactic. In the following instance declaration, I expect that <code>setoid_rewrite fmapComp</code> would rewrite <code>fmap iso ∘ fmap inv</code> to <code>fmap (iso ∘ inv)</code>. However, Coq reports that "no progress was made" during rewriting:</p>
  
  <pre><code>Instance functorsPreserveIsomorphisms
   `{C : Cat o η} `{D : Cat u ρ}
     {a b : o} {φ : o → u} (F : Functor C D φ) (I : a ≅ b) : φ a ≅ φ b.
  Proof.
    apply (Build_Isomorphism _ _ _ (φ a) (φ b) (fmap iso) (fmap inv)).
  
   o : Type
   η : o → o → Type
   C : Cat o η
   u : Type
   ρ : u → u → Type
   D : Cat u ρ
   a : o
   b : o
   φ : o → u
   F : Functor C D φ
   I : a ≅ b
   ============================
    fmap iso ∘ fmap inv ≡ id (φ a)
  </code></pre>
  
  <p>I don't understand why <code>setoid_rewrite</code> fails. For reference, the <em>same</em> command works in other contexts using the <em>same</em> terms. For example, it rewrites either side of the following goal to the other:</p>
  
  <pre><code>Lemma worksotherwise
   `{C : Cat o η} `{D : Cat u ρ}
     {a b : o} {φ : o → u} (F : Functor C D φ) (I : a ≅ b) :
       fmap iso ∘ fmap inv ≡ fmap (iso ∘ inv)
  
   o : Type
   η : o → o → Type
   C : Cat o η
   u : Type
   ρ : u → u → Type
   D : Cat u ρ
   a : o
   b : o
   φ : o → u
   F : Functor C D φ
   I : a ≅ b
   ============================
    fmap iso ∘ fmap inv ≡ fmap (iso ∘ inv)
  </code></pre>
  
  <p>It's unclear why <code>setoid_rewrite</code> works in the second case but not the first. For reference, <code>≡</code> is <code>equiv</code> and <code>fmap</code> is <code>Proper</code>. Other than that <code>≅</code>, <code>Functor</code> and <code>Cat</code> are classes, I don't see any other relevant facts. Also, <code>setoid_replace</code> works fine.</p>