Definition iterop_list_list : list(list X) → X. Proof. intros w. exact (iterop_list (map iterop_list w)). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.NegativePropositions.