proposition: Lemma nth_append_L A: forall n m (v : t A n) (w : t A m) p, (v ++ w) [@ Fin.L m p] = v [@ p].
proof: Proof. intros n m v w. induction v as [|a n v IH]. - apply Fin.case0. - intros p. now apply (Fin.caseS' p). Qed.
imports: VectorDef PeanoNat Eqdep_dec