proposition: Lemma take_prf_irr : forall {A} p {n} (v:t A n) le le', take p le v = take p le' v.
proof: Proof. intros A p; induction p as [|p IHp]; intros n v le le'. - reflexivity. - destruct v. + inversion le. + simpl. apply f_equal, IHp. Qed.
imports: VectorDef PeanoNat Eqdep_dec