# Confused with a failure of a generalized rewrite

**URL:** https://discourse.rocq-prover.org/t/confused-with-a-failure-of-a-generalized-rewrite/783
**Category:** Using Rocq
**Created:** [April 15, 2020, 10:17pm UTC](https://discourse.rocq-prover.org/t/confused-with-a-failure-of-a-generalized-rewrite/783 "2020-04-15T22:17:27Z")
**Posts on this page:** 1
**Showing post:** 3

<div class="post-metadata">

### Author: ![Yannick](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/yannick/32/321_2.png) [@Yannick](https://discourse.rocq-prover.org/u/Yannick)
#### Post date: [April 21, 2020, 8:54pm UTC](https://discourse.rocq-prover.org/t/confused-with-a-failure-of-a-generalized-rewrite/783/3 "2020-04-21T20:54:01Z")

</div>

Hi @Blaisorblade ,

Thanks a lot for your answer!  
However, as much as this connex question is also very much of interest to me as well, I do not believe it to be directly related to this issue at hand.

The instance `eq_rel_rewrite` does allow extensional rewriting in this context, which actually is what happens in the first Goal (I rewrite `R ≡ S` in the goal `R x y` by virtue of the `pointwise_relation` part of the instance).

The failure is the exact same case, but instantiated with slightly more complex “R” and “S”. The equation `F († R) ≡ † (F R)` is already in my context, I do not need to derive it.

Best,  
Yannick

---

_[View the full topic](https://discourse.rocq-prover.org/t/confused-with-a-failure-of-a-generalized-rewrite/783)._