proposition: Lemma Vreplace_tail : forall n i (ip : S i < S n) (v : vector A (S n)) a, Vreplace v ip a = Vcons (Vhead v) (Vreplace (Vtail v) (NatCompat.lt_S_n ip) a).
proof: Proof. destruct n; intros. lia. VSntac v. refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)