Commit 2021-02-25 15:43 85b5d5cb
View on Github →refactor(logic/basic): turn prop_of into congr lemma (#6406) Alternative solution to the exists part of #6404.
refactor(logic/basic): turn prop_of into congr lemma (#6406) Alternative solution to the exists part of #6404.