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 autorewrite with nth. 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