Commit 2024-03-08 07:00 c697e040

chore: Remove ball and bex from lemma names (#10816) ball for "bounded forall" and bex for "bounded exists" are from experience very confusing abbreviations. This PR renames them to forall_mem and exists_mem in the few Set lemma names that mention them. Also deprecate ball_image_of_ball, mem_image_elim, mem_image_elim_on since those lemmas are duplicates of the renamed lemmas (apart from argument order and implicitness, which I am also fixing by making the binder in the RHS of forall_mem_image semi-implicit), have obscure names and are completely unused.