proposition: Lemma nth_vmap {A B n} (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: Equations(CoreTactics) Equations.HoTT.All Equations.HoTT.WellFounded Coq.Unicode.Utf8 HoTT.Types.Bool HoTT.Spaces.Nat HoTT.Classes.implementations.peano_naturals Equations.HoTT.Tactics