Definition iterop_fun_step' (lunax : islunit op unel) {m} (xs:stn m → X) (x:X) : iterop_fun (append_vec xs x) = op (iterop_fun xs) x. Proof. unfold iterop_fun at 1. simpl. induction m as [|m _]. - simpl. rewrite append_vec_compute_2. apply pathsinv0. apply lunax. - simpl. rewrite append_vec_compute_2. apply (maponpaths (λ y, op y x)). apply maponpaths. apply append_and_drop_fun. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.NegativePropositions.