Rewrite set equality inside a let expression

Using Coq
1

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:

 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.

2

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:

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.

3

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.