proposition: Lemma IndexBound_AppendR {A n m} : forall (Bound : Vector.t A n) (Bound' : Vector.t A m) (idx : Fin.t n), Vector.nth (Vector.append Bound Bound') (Fin.L m idx) = Vector.nth Bound idx.
proof: Proof. induction Bound; intros. - inversion idx. - revert Bound IHBound; pattern n, idx; apply Fin.caseS; simpl; intros; eauto. Qed.
imports: Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Coq.Logic.Eqdep_dec Fiat.Common.ilist Fiat.Common.ilist2