Commit 2021-04-07 02:18 97832daf
View on Github →chore(logic/function/basic): remove classical decidable instance from a lemma statement (#6488)
Found using #6485
This means that this lemma can be use in reverse against any ite, not just one that uses classical.decidable.