proposition: Lemma collect_ssf: forall a acc, collect (ssf a) acc [=] collect a acc.
proof: Proof. induction a; simpl; unfold dot', plus_but_one, star'; intro acc; auto; RegExp.destruct_tests; simpl; auto. rewrite <- IHa1, IHa2. reflexivity. rewrite <- IHa2, IHa1. reflexivity. rewrite IHa1, IHa2. reflexivity. rewrite IHa1, IHa2. reflexivity. rewrite <- IHa. rewrite <- collect_ssf_remove. rewrite (RegExp.Is_one O). reflexivity. rewrite collect_ssf_remove, IHa. reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(DKA_Definitions) ATBR(StrictStarForm)