remove cbvaldOLD since: obsolete for more than a year, proof has no advantage whatsoever over cbvdald. On the other hand, not that cbvex2OLD (which has been obsolete for only a few days anyway) has the (tiny) advantage over cbvex2 of not using the negation connective.
remove cbvaldOLD since: obsolete for more than a year, proof has
no advantage whatsoever over cbvdald. On the other hand, not that
cbvex2OLD (which has been obsolete for only a few days anyway)
has the (tiny) advantage over cbvex2 of not using the negation
connective.

metamath/set.mm,metamath/set.mm,metamath/set.mm