proposition: Lemma tval_tcast (T : Type) (n m : nat) (e : n = m) (t : n.-tuple T): tval (tcast e t) = tval t.
proof: Proof. by case: m / e. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset order) mathcomp(ssralg)