proposition: Lemma Vnth_cast : forall n (v : vector A n) n' (e : n = n') k (h : k < n'), Vnth (Vcast v e) h = Vnth v (Vnth_cast_aux e h).
proof: Proof. induction v as [|x p v IHv]. intros; lia. intros [|n']; try discr. inversion e; subst p; intros [|k] h; rewrite Vcast_refl; simpl. refl. rewrite (IHv n' (eq_refl n') k); apply Vnth_eq; refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)