refactor: remove funext dependency from Classical.em, drop Quot.sound - #14420

refactor: remove funext dependency from Classical.em, drop Quot.sound#14420

tchaumeny wants to merge 4 commits into

leanprover:masterleanprover/lean4:masterfrom

tchaumeny:diaconescu_reworktchaumeny/lean4:diaconescu_reworkCopy head branch name to clipboard