proposition: Lemma flatten_valid `(M: @EMonoid A op one eqv): forall t , eval M t == eval M (flatten t).
proof: Proof. add_op_proper M HM; induction t;simpl. - rewrite <- flatten_aux_valid, <- IHt2; reflexivity. - reflexivity. - monoid_simpl M;reflexivity. Qed.
imports: Coq(Relations RelationClasses Lia List) Param(Param) additions(More_on_positive)