proposition: Lemma vector_rect : forall (P: forall dim, vector dim -> Type) (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. fix vector_rect 1;intros [|dim]. exact f1. simpl. intros [a v]. apply f2. apply vector_rect. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)