Definition iterop_fun_fun {n} {m:stn n → nat} : (∏ i (j:stn (m i)), X) → X. Proof. intros x. exact (iterop_fun (λ i, iterop_fun (x i))). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.NegativePropositions.