proposition: Lemma collect_ssf_remove: forall a acc, collect (remove a) acc [=] collect a acc.
proof: Proof. induction a; simpl; intro acc; auto. case contains_one; simpl; auto. case contains_one; simpl; auto. unfold plus_but_one. RegExp.destruct_tests; simpl; auto. rewrite <- IHa1, IHa2. reflexivity. rewrite <- IHa2, IHa1. reflexivity. rewrite IHa1, IHa2. reflexivity. case contains_one; simpl; auto. unfold plus_but_one. RegExp.destruct_tests; simpl; auto. rewrite <- IHa1, IHa2. reflexivity. rewrite <- IHa2, IHa1. reflexivity. rewrite IHa1, IHa2. reflexivity. case contains_one; simpl; auto. unfold plus_but_one. RegExp.destruct_tests; simpl; auto. rewrite <- IHa1, IHa2. reflexivity. rewrite <- IHa2, IHa1. reflexivity. rewrite IHa1, IHa2. reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(DKA_Definitions) ATBR(StrictStarForm)