Maybe I'm rusty, but I've hard time finding the proof of this one. Do you think it is worth adding ?

```
Lemma tval_tcastE m n (eq_mn : m = n) (t : m.-tuple T) :
tcast eq_mn t = t :> seq T.
Proof. by case: n / eq_mn. Qed.
```

Florent Hivert said:

Maybe I'm rusty, but I've hard time finding the proof of this one. Do you think it is worth adding ?

`Lemma tval_tcastE m n (eq_mn : m = n) (t : m.-tuple T) : tcast eq_mn t = t :> seq T. Proof. by case: n / eq_mn. Qed.`

I vote +1 for the proposal, since I needed it once and Emilio had to show me the proof, which was not obvious to me. It would be useful to beginners.

Last updated: Feb 08 2023 at 04:04 UTC