proposition: Lemma Vnth_remove_last : forall n (v : vector A (S n)) i (h : i<n), Vnth (Vremove_last v) h = Vnth v (Nat.lt_lt_succ_r h).
proof: Proof. intros n v i h. sym. apply Vnth_remove_last_intro. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)