proposition: Lemma collect_idem: forall a acc, collect a (collect a acc) [=] collect a acc.
proof: Proof. induction a; simpl; intro; try reflexivity. rewrite (collect_com a2 a1). rewrite IHa1, IHa2. reflexivity. rewrite (collect_com a2 a1). rewrite IHa1, IHa2. reflexivity. apply IHa. NumSetProps.setdec. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(DKA_Definitions) ATBR(StrictStarForm)