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