proposition: Lemma Vnth_addl : forall k n (v : vector A n) a (H1 : k < S n) (H2 : k < n), Vnth (Vadd v a) H1 = Vnth v H2.
proof: Proof. intros. assert (H3 : H1 = (@le_S (S k) n H2)). apply lt_unique. subst H1. generalize dependent k. generalize dependent n. intro n. elim n. intros v k H. exfalso. apply (Nat.nlt_0_r H). intros n' Hrec v k H. rewrite (VSn_eq v). destruct k. simpl. refl. simpl Vadd. assert (H' : k < S n'). auto with arith. simpl. assert (NatCompat.lt_S_n (le_S H) = le_S (NatCompat.lt_S_n H)). apply lt_unique. rewrite H0, Hrec. refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)