proposition: Lemma iterop_seq_mon_homot {n} (x y : stn n -> M) : x ~ y -> iterop_seq_mon(n,,x) = iterop_seq_mon(n,,y).
proof: Proof. revert x y. induction n as [|n N]. - reflexivity. - intros x y h. rewrite 2 iterop_seq_mon_step. apply two_arg_paths. + apply N. apply funhomot. exact h. + apply h. Defined.
imports: UniMath.Combinatorics.Lists UniMath.Combinatorics.FiniteSequences UniMath.Algebra.RigsAndRings UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Tactics UniMath.Algebra.Groups UniMath.MoreFoundations.NegativePropositions