proposition: Lemma VLSet_to_X_compat: forall i j, VLSet.eq i j -> equal (VLSet_to_X i) (VLSet_to_X j).
proof: Proof. intros. apply (VLSetProps.fold_equal _ Hpc). assumption. Qed.
imports: ATBR(MyFSets MyFSetProperties) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(Numbers) ATBR(Reification)