proposition: Lemma remove_strict: forall a, strict_star_form a -> RegExp.is_one (remove a) = false -> strict (remove a).
proof: Proof. induction 1; simpl; auto. unfold plus_but_one. case_eq (contains_one a); intro Ha; simpl. RegExp.destruct_tests; auto. case_eq (contains_one b); intro Hb; simpl; auto. RegExp.destruct_tests; auto. unfold plus_but_one. case_eq (contains_one a); intro Ha; simpl; auto. case_eq (contains_one b); intro Hb; simpl; auto. RegExp.destruct_tests; auto. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(SemiLattice) ATBR(Monoid) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(Model_RegExp) Coq(Bool)