proposition: Lemma nth_vmap `(v : vector A n) `(fn : A -> B) (f : fin n) : nth (vmap fn v) f = fn (nth v f).
proof: Proof. revert B fn. funelim (nth v f); intros; now simp nth vmap. Qed.
imports: Program Bvector List Relations Equations(Equations Signature) Utf8 Arith Wf_nat Bvector Examples.Fin