Commit 2024-07-09 23:50 b7deda7f

feat(Logic/Basic): add simp lemma for @Exists.choose _ (· = a) _ (#14419) and for the symmetric case.