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