Is there a more elegant way to get to `eq_from_tnth`

than what is done in this code snippet?

```
From Coq Require Import Unicode.Utf8.
From mathcomp Require Import all_ssreflect.
From mathcomp.fingroup Require Import perm.
From Coq Require Import ssrsearch.
Variable (n : nat).
Lemma foo (x y : n.-tuple nat) (p : 'S_n) : perm_eq x y.
Proof.
apply/tuple_permP.
exists p.
(**)
set xx := (X in val X = _); set yy := (X in _ = val X).
suff : xx = yy by move=> ->.
(**)
apply: eq_from_tnth => j.
```

Thanks.

This could maybe replace the last 3 lines: `rewrite -[X in _ = _ X](@eq_from_tnth _ _ x) // => j.`

Nice :) Thanks a lot.

This should also work

```
congr (val _).
apply: eq_from_tnth => j.
```

Enrico Tassi said:

This should also work

`congr (val _). apply: eq_from_tnth => j.`

Damned, of course! `congr val`

is even enough. Thanks a lot :)

Last updated: Jul 15 2024 at 21:02 UTC