proposition: Lemma assoc_seq_to_fun : isAssociative_seq -> isAssociative_fun.
proof: Proof. intros assoc n m x. exact (assoc (functionToSequence (λ i, functionToSequence (x i)))). Defined.
imports: UniMath.Combinatorics.Lists UniMath.Combinatorics.FiniteSequences UniMath.Algebra.RigsAndRings UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Tactics UniMath.Algebra.Groups UniMath.MoreFoundations.NegativePropositions