Commit 2021-08-25 06:39 26a32863
View on Github →fix(data/set/lattice): lemmas about Union/Inter over p : Prop (#8860)
With recently added @[congr] lemmas, it suffices to deal with unions/inters over true and false.
fix(data/set/lattice): lemmas about Union/Inter over p : Prop (#8860)
With recently added @[congr] lemmas, it suffices to deal with unions/inters over true and false.