fact: Definition eta_vector@{i j k} {A : Type@{i}} (P : forall n : nat, vector@{i} A n -> Type@{j}) : forall (n : nat) (v : vector@{i} A n), paths@{k} (match v return Type@{j} with | nil => P 0 nil | cons n a v => P _ (cons a v) end) (P n v).
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