# Rewrite set equality inside a let expression

**URL:** <https://discourse.rocq-prover.org/t/rewrite-set-equality-inside-a-let-expression/2013>\
**Category:** Using Rocq\
**Created:** [August 19, 2023, 5:15pm UTC](https://discourse.rocq-prover.org/t/rewrite-set-equality-inside-a-let-expression/2013 "2023-08-19T17:15:18Z")\
**Posts on this page:** 5\
**Page:** 1

<div class="post-metadata">

**Author:** ![flaviodemoura](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/flaviodemoura/32/391_2.png) [@flaviodemoura](https://discourse.rocq-prover.org/u/flaviodemoura)\
**Post date:** [August 19, 2023, 5:15pm UTC](https://discourse.rocq-prover.org/t/rewrite-set-equality-inside-a-let-expression/2013/1 "2023-08-19T17:15:18Z")

</div>

Hello! Is it possible to make a rewriting inside a let expression that in turn is inside an Inductive definition? More precisely, I am using the Metalib package where [=] represents set equality. I have an hypothesis of the form H: a [=] b, and I want to replace some occurrences of a for b (rewrite H) inside a let expression that, in turn, is inside an Inductive definition. My current proof context is:

```auto
 Hfv : fv_nom u [=] fv_nom u'
  ============================
  (let (z, _) := atom_fresh (union (fv_nom u) (union (fv_nom (n_abs y t1)) (singleton x))) in
   n_abs z (subst_rec_fun (swap y z t1) u x)) =a
  (let (z, _) := atom_fresh (union (fv_nom u') (union (fv_nom (n_abs y t1)) (singleton x))) in
   n_abs z (subst_rec_fun (swap y z t1) u' x))

```

where =a is an inductive predicate. I want to replace (fv\_nom u) for (fv\_nom u’) in the goal. When I try to “rewrite Hfv” I get Error: build\_signature: no constraint can apply on a dependent argument.

Thank you in advance!

Regards,  
Flávio.

---

<div class="post-metadata">

**Author:** ![flaviodemoura](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/flaviodemoura/32/391_2.png) [@flaviodemoura](https://discourse.rocq-prover.org/u/flaviodemoura)\
**Post date:** [August 19, 2023, 10:52pm UTC](https://discourse.rocq-prover.org/t/rewrite-set-equality-inside-a-let-expression/2013/2 "2023-08-19T22:52:38Z")

</div>

Hi! As a complement to the previous question: the problem is in fact related to the let expression. The following example shows that even if the inductive =a is not in the context, the problem remain the same:

```auto
Parameter a b: atom.
Lemma test: (singleton a) [=] (singleton b) -> let (x,_) := atom_fresh (singleton a) in True.
Proof.
 intro H. Fail rewrite H.

The command has indeed failed with message:
build_signature: no constraint can apply on a dependent argument

```

Any help is very welcome.

Regards,  
Flávio.

---

<div class="post-metadata">

**Author:** ![herbelin](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/herbelin/32/111_2.png) [@herbelin](https://discourse.rocq-prover.org/u/herbelin)\
**Post date:** [August 30, 2023, 8:12pm UTC](https://discourse.rocq-prover.org/t/rewrite-set-equality-inside-a-let-expression/2013/3 "2023-08-30T20:12:37Z")

</div>

Hum, For the short example, I’m afraid this is a limitation of “setoid rewriting”. Maybe using a definition `LET : forall A B, forall a:A, (forall a:A, B a) -> B a`.

Another solution would be to first rewrite `atom_fresh (singleton a)` into `pair (fst (atom_fresh (singleton a)) (snd (atom_fresh (singleton a)))` (for whatever constructor `pair` and projections `fst` and `snd` available in your type). The `let` would then reduce.

---

<div class="post-metadata">

**Author:** ![flaviodemoura](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/flaviodemoura/32/391_2.png) [@flaviodemoura](https://discourse.rocq-prover.org/u/flaviodemoura)\
**Post date:** [February 25, 2026, 4:56pm UTC](https://discourse.rocq-prover.org/t/rewrite-set-equality-inside-a-let-expression/2013/4 "2026-02-25T16:56:16Z")

</div>

Sorry to revisit this old question, but I still haven’t found a satisfactory solution. Back in 2023, I was using Coq 8.? and now with Rocq 9.1.1, I’m still unable to use setoid rewriting inside the body of a let expression. The error message is the same.

To clarify: I need to perform the rewrite \*before\* evaluating the let expression. Concretely, I have a hypothesis

> H: t [=] u

(with a user-defined equality [=]) and a goal containing a let expression as follows:

> let x := r in s

where r may have occurrencesof t. Before evaluating the let expression, I would like to rewrite H and replace all occurrences of t in r by u, and then evaluate the let expression.

Above, Herbelin suggested this might be a limitation of setoid rewriting. So my question is: should I expect this limitation to be permanent? Is there a logical/theoretical issue that prevents setoid rewriting in the body of a let expression?

Best regards,

Flávio.

---

<div class="post-metadata">

**Author:** ![SkySkimmer](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/skyskimmer/32/369_2.png) [@SkySkimmer](https://discourse.rocq-prover.org/u/SkySkimmer)\
**Post date:** [February 25, 2026, 6:40pm UTC](https://discourse.rocq-prover.org/t/rewrite-set-equality-inside-a-let-expression/2013/5 "2026-02-25T18:40:11Z")

</div>

May be solved by [Support generalized rewriting in let bindings by mattam82 · Pull Request #20985 · rocq-prover/rocq · GitHub](https://github.com/rocq-prover/rocq/pull/20985) (not yet merged)