Description: Obsolete version of raleqbidvv as of 9-Mar-2025. (Contributed by BJ, 22-Sep-2024) (New usage is discouraged.) (Proof modification is discouraged.)