proposition: Lemma collect_incr_2: forall a i acc, NumSet.In i acc -> NumSet.In i (collect a acc).
proof: Proof. induction a; simpl; intros; auto. NumSetProps.setdec. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(DKA_Definitions) ATBR(StrictStarForm)