This fix is probably not enough to justify that there are no problems with

primitive projections and prop. ext. or univalence, but at least it prevents
known proofs of false (see discussion on #4588).

0 files changed, 0 insertions, 0 deletions