proposition: Theorem ssf_complete: forall a, strict_star_form (ssf a).
proof: Proof. induction a; simpl; auto. unfold dot'. RegExp.destruct_tests; auto. unfold star'. RegExp.destruct_tests; auto. constructor. apply remove_nf; trivial. apply remove_strict; trivial. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(SemiLattice) ATBR(Monoid) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(Model_RegExp) Coq(Bool)