proposition: Lemma shiftin_nth A a n (v: t A n) k1 k2 (eq: k1 = k2): nth (shiftin a v) (Fin.L_R 1 k1) = nth v k2.
proof: Proof. subst k2; induction k1 as [n|n k1 IH]. - revert n v. now apply caseS. - revert k1 IH. apply (fun P IS => caseS P IS v). now simpl. Qed.
imports: VectorDef PeanoNat Eqdep_dec