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