proposition: Lemma str_pls_str `{laws} `{KA ≪ l} n (x y: X n n): (x+y)^* ≡ (x^* + y^* )^* .
proof: Proof. symmetry. rewrite str_pls, str_invol, <-str_pls. rewrite cupC. now rewrite str_pls, str_invol, <-str_pls, cupC. Qed.
imports: monoid