mathlib3

feat(logic/relation): auxiliary `forall_exists_rel` relation

#18713

Open