fact: Definition hdrop {n:nat} {P: ⟦ S n ⟧ → UU} (f: ∏ i: ⟦ S n ⟧, P i) : (∏ i: ⟦ n ⟧, P (dni_firstelement i)) := f ∘ dni_firstelement.
imports: UniMath.Foundations.All UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Vectors