mathlib
85b5d5cb - refactor(logic/basic): turn _prop_of_ into congr lemma (#6406)

Commit

5 years ago

refactor(logic/basic): turn *_prop_of_* into congr lemma (#6406) Alternative solution to the exists part of #6404.

Author

gebner

Parents

mathlib 85b5d5cb - refactor(logic/basic): turn *_prop_of_* into congr lemma (#6406)