proposition: Theorem complete: forall a b, same_labels (clean a) (clean b) = false -> ~ a == b.
proof: Proof. intros a b H H'. assert (F := equal_collect H' NumSet.empty). apply NumSet.equal_1 in F. unfold same_labels in H. rewrite F in H. discriminate. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(DKA_Definitions) ATBR(StrictStarForm)