proposition: Theorem decide_correct: forall x y, decide x y = true -> equal x y.
proof: Proof. intros x y H. transitivity (norm x); [ apply norm_correct | ]. transitivity (norm y); [ | symmetry; apply norm_correct ]. apply VLSet_to_X_compat. apply VLSet.equal_2. assumption. Qed.
imports: ATBR(MyFSets MyFSetProperties) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(Numbers) ATBR(Reification)