Skip to content

[Merged by Bors] - feat(Logic/Basic): add simp lemma for @Exists.choose _ (· = a) _ #47264

[Merged by Bors] - feat(Logic/Basic): add simp lemma for @Exists.choose _ (· = a) _

[Merged by Bors] - feat(Logic/Basic): add simp lemma for @Exists.choose _ (· = a) _ #47264

Annotations

9 warnings

This job succeeded