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