proposition: Lemma cast_eq {A} {n p} (v : t A n) (w : t A p) (e : n = p): v == w -> w = cast v p e.
proof: Proof. intros. apply equiv_eq. subst p. red. transitivity (to_list v); auto. apply equiv_cast. Qed.
imports: Bool Arith Vector