Definition iterop_fun {n} (x:stn n->X) : X. Proof. intros. induction n as [|n _]. { exact unel. } { induction n as [|n I]. { exact (x lastelement). } { exact (op (I (x ∘ dni lastelement)) (x lastelement)). }} Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.NegativePropositions.