feat: remove Quot.sound axiom from em, provide em_eq without propext#13826

lyphyser wants to merge 2 commits into

leanprover:masterleanprover/lean4:masterfrom

lyphyser:em_eqlyphyser/lean4:em_eqCopy head branch name to clipboard