proposition: Lemma vector_ind : forall (P: forall dim, vector dim -> Prop) (f1: forall v, P 0 v) (f2: forall dim a v, P _ v -> P (S dim) (a,v)) dim v, P dim v.
proof: Proof. intros P f1 f2 dim v. apply vector_rect;assumption. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)