Hi,

How can I do the equivalent of

```
rewrite ?H, ?H2 in *.
```

but with setoid_rewrite?

Hi,

How can I do the equivalent of

```
rewrite ?H, ?H2 in *.
```

but with setoid_rewrite?

1 Like

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:

```
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?

Thanks for your answer.

Yes due to type classes mismatches I am in a situation where only setoid_rewrite works.