How to compose setoid_rewrite?

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.


Require Import Setoid.

Goal forall P Q R, (P <-> Q) -> (Q <-> R) -> (Q <-> Q) -> P -> R.
  intros P Q R H H0 H1 H2.
  rewrite ?H0, ?H1 in *.
  apply H, H2.

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.