# Setoid rewriting with implications
**URL:** https://discourse.rocq-prover.org/t/setoid-rewriting-with-implications/913
**Category:** Using Rocq
**Created:** [July 1, 2020, 1:12pm UTC](https://discourse.rocq-prover.org/t/setoid-rewriting-with-implications/913 "2020-07-01T13:12:02Z")
**Posts on this page:** 2
**Page:** 1
### Author:  [@Ptival](https://discourse.rocq-prover.org/u/Ptival)
#### Post date: [July 1, 2020, 1:12pm UTC](https://discourse.rocq-prover.org/t/setoid-rewriting-with-implications/913/1 "2020-07-01T13:12:02Z")
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.
---
### Author:  [@mattam82](https://discourse.rocq-prover.org/u/mattam82)
#### Post date: [July 1, 2020, 1:48pm UTC](https://discourse.rocq-prover.org/t/setoid-rewriting-with-implications/913/2 "2020-07-01T13:48:10Z")
That’s indeed unfortunate that `setoid_rewrite` expects a lemma of the form `(forall ..., R x y)` and attempts only to rewrite with `R` rather than the implication relation, but changing this would involve a lot of incompatibilities I suspect. You should be able to use a helper lemma of type `to_impl: forall {A B}, (A -> B) -> impl A B` to turn an existing lemma into an explicit `impl` version and rewrite with `to_impl (lemma _ .. _)` intead.