proposition: Lemma tcast_trans m n p (eq_mn : m = n) (eq_np : n = p) t: tcast (etrans eq_mn eq_np) t = tcast eq_np (tcast eq_mn t).
proof: Proof. by case: n / eq_mn eq_np; case: p /. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype path)