Hi!

I just encountered a limitation that I don’t quite understand the justification for, and would like to know more about it.

Boiled down, the problem is rewriting with an implication in a product:

```
From Coq Require Import Morphisms.
From Coq Require Import Program.
Goal forall (A B C : Prop) (H : A /\ B) (P : B -> C), A /\ C.
intros.
setoid_rewrite P in H. (* fails *)
```

After a bit of a head scratch, and having been able to do this manually by calling `Morphisms_Prop.and_impl_morphism`

, I was wondering whether I could help by folding `->`

into `impl`

, and indeed, it works:

```
From Coq Require Import Morphisms.
From Coq Require Import Program.
Goal forall (A B C : Prop) (H : A /\ B) (P : B -> C), A /\ C.
intros.
assert (impl B C) as P' by exact P.
setoid_rewrite P' in H.
```

What is the reason for this limitation? Is there a known trick to force this rewrite to happen?

It is particularly annoying when `P`

is not a local assumption, but some existing lemma you’d like to rewrite with.