proposition: Lemma str_unfold_l `{laws} `{KA ≪ l} n (x: X n n): x^* ≡ 1+x⋅x^*.
proof: Proof. apply antisym. apply str_ind_l1. lattice. rewrite dotxpls. apply leq_cupx. rewrite <-str_refl. lattice. rewrite <-str_cons at 2. lattice. rewrite str_cons, (str_refl x). lattice. Qed.
imports: lattice