proposition: Lemma collect_incr_1: forall a i acc acc', NumSet.In i (collect a acc') -> NumSet.In i (collect a acc) \/ NumSet.In i acc'.
proof: Proof. induction a; simpl; intros i acc acc' Hi; auto. eapply IHa1 in Hi as [Hi|Hi]. left. apply Hi. eapply IHa2 in Hi as [Hi|Hi]; auto. left. apply collect_incr_2, Hi. eapply IHa1 in Hi as [Hi|Hi]. left. apply Hi. eapply IHa2 in Hi as [Hi|Hi]; auto. left. apply collect_incr_2, Hi. NumSetProps.setdec. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(DKA_Definitions) ATBR(StrictStarForm)