proposition: Lemma list_join_app `{Setoid A} (l k : list (list A)) : join (l & k) = join l & join k.
proof: Proof. unfold join, list_join, sg_op, list_app. induction l; simpl; try reflexivity. now rewrite IHl, app_assoc. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.monads