proposition: Lemma nth_vtail `(v : vector A (S n)) (f : fin n) : nth (vtail v) f = nth v (fs f).
proof: Proof. funelim (vtail v); intros; now simp nth. Qed.
imports: Program Bvector List Relations Equations(Equations Signature) Utf8 Arith Wf_nat Bvector Examples.Fin