mathlib3
3c224f0c - feat (logic/basic): exists_eq' (#1397)

Commit
6 years ago
feat (logic/basic): exists_eq' (#1397) Not a great name, but `exists_eq_left` and `exists_eq_right` are taken, and it's unlikely to be used except in `simp`
Author
Committer
Parents
Loading