proposition: Lemma expand_simple e: is_simple e -> e ≡ eps e + pure_part e.
proof: Proof. induction 1; simpl; fold_regex. lattice. lattice. lattice. rewrite orb_pls. rewrite IHis_simple1 at 1. rewrite IHis_simple2 at 1. lattice. rewrite andb_dot. rewrite (@expand_01 e) at 1 by assumption. rewrite IHis_simple at 1. ra. rewrite cupxb. rewrite (@expand_01 e) at 1 by assumption. apply str_eps. Qed.
imports: syntax kleene boolean lang lset sums normalisation