Definition iterop_fun_append (lunax : islunit op unel) {m} (x:stn m → X) (y:X) : iterop_fun (append_vec x y) = op (iterop_fun x) y. Proof. rewrite (iterop_fun_step lunax). rewrite append_vec_compute_2. apply (maponpaths (λ x, op (iterop_fun x) y)). apply funextfun; intro i. simpl. rewrite append_vec_compute_1. reflexivity. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.NegativePropositions.