proposition: Theorem same_labels_ssf: forall a b, same_labels a b = true -> same_labels (ssf a) (ssf b) = true.
proof: Proof. intros. unfold same_labels. rewrite 2 collect_ssf. assumption. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(DKA_Definitions) ATBR(StrictStarForm)