proposition: Lemma equiv_cast : forall (A:Type) n (v : t A n) n' (e: n = n'), v == cast v n' e.
proof: Proof. induction v. - intros; now subst. - intros; subst; simpl; red ; repeat rewrite to_list_cons. f_equal; apply (IHv n). Qed.
imports: Bool Arith Vector