# How to compose setoid\_rewrite?
**URL:** https://discourse.rocq-prover.org/t/how-to-compose-setoid-rewrite/290
**Category:** Using Rocq
**Created:** [May 17, 2019, 8:12am UTC](https://discourse.rocq-prover.org/t/how-to-compose-setoid-rewrite/290 "2019-05-17T08:12:30Z")
**Posts on this page:** 3
**Page:** 1
### Author:  [@Matafou](https://discourse.rocq-prover.org/u/Matafou)
#### Post date: [May 17, 2019, 8:12am UTC](https://discourse.rocq-prover.org/t/how-to-compose-setoid-rewrite/290/1 "2019-05-17T08:12:30Z")
Hi,
How can I do the equivalent of
```auto
rewrite ?H, ?H2 in *.
```
but with setoid\_rewrite?
---
### Author:  [@yforster](https://discourse.rocq-prover.org/u/yforster)
#### Post date: [May 17, 2019, 11:22am UTC](https://discourse.rocq-prover.org/t/how-to-compose-setoid-rewrite/290/2 "2019-05-17T11:22:26Z")
This might be too naive of an answer, but since `rewrite` falls back to `setoid_rewrite` if the relation is not equality, the equivalent is the exact same code.
See:
```auto
Require Import Setoid.
Goal forall P Q R, (P <-> Q) -> (Q <-> R) -> (Q <-> Q) -> P -> R.
Proof.
intros P Q R H H0 H1 H2.
rewrite ?H0, ?H1 in *.
apply H, H2.
Qed.
```
Or are you in a situation where the relation has equality deep down and `rewrite` does not fall back to `setoid_rewrite` automatically?
---
### Author:  [@Matafou](https://discourse.rocq-prover.org/u/Matafou)
#### Post date: [May 17, 2019, 11:25am UTC](https://discourse.rocq-prover.org/t/how-to-compose-setoid-rewrite/290/3 "2019-05-17T11:25:15Z")
Thanks for your answer.
Yes due to type classes mismatches I am in a situation where only setoid\_rewrite works.