proposition: Lemma IndexBound_AppendL {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.R m idx) = Vector.nth Bound idx.
proof: Proof. induction Bound'; intros. - reflexivity. - simpl; eauto. Qed.
imports: Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Coq.Logic.Eqdep_dec Fiat.Common.ilist Fiat.Common.ilist2