I'm in a bind with a goal equality like this (the details don't matter, I think):
tcast tc0
[tuple of take i (s_bs bs) ++ drop i.+1 (s_bs bs) ++ [:: [ffun⇒ 0]]]
=
...
How do I get rid of the tcast and tuple to go back to simple seq (I tried the val_inj trick, but this didn't seem to remove the type cast)?
Thanks in advance.
Bye,
Pierre
Giving a precise answer is a bit difficult, since you did not provide any reproducible testcase. But you could try rewriting your goal using the following lemma, once you have applied val_inj.
Lemma val_tcast {T} m n (tc : n = m) (x : n.-tuple T) :
val (tcast tc x) = val x.
Proof. now case tc. Qed.