Commit 2022-12-26 18:42 0de015fb
View on Github →feat: port data.set.intervals.pi (#1223)
I changed a single proof, Icc_diff_pi_univ_Ioo_subset
because the simpa
got lost somewhere along the way. It did produce an existential statement in the end but it was not the correct one it seems. Since the proof was easy enough to fix without simpa
I just did that instead of figuring out what exactly is going wrong.