proposition: Theorem associativityOfProducts_list (M:monoid) : isAssociative_list (unel M) (@op M).
proof: Proof. unfold isAssociative_list. apply list_ind. - simpl. reflexivity. - intros x xs I. simpl in I. rewrite Lists.flattenStep. refine (iterop_list_mon_concatenate _ _ @ _). unfold iterop_list_list. rewrite mapStep. rewrite (iterop_list_step _ _ (runax M)). + apply (maponpaths (λ x, _ * x)). exact I. Defined.
imports: UniMath.Combinatorics.Lists UniMath.Combinatorics.FiniteSequences UniMath.Algebra.RigsAndRings UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Tactics UniMath.Algebra.Groups UniMath.MoreFoundations.NegativePropositions