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: Mar 29 2024 at 11:01 UTC