[Merged by Bors] - chore: clear some porting notes on rfl

[mo271]

We remove some porting notes for rfls that by now work again.

---

[mo271]

It seems like two cases where a proof was broken during the port, and it was suspected that leanprover-community/batteries#62 was the reason now work again. So it seems the underlying cause of breakage might have been something else.

[eric-wieser]

!bench

[eric-wieser]

bors d+

I've seen cases where a convert proof for decidability instance is incredibly slow.

[bors]

✌️ mo271 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[leanprover-bot]

Here are the benchmark results for commit aead19d.
There were no significant changes against commit f8593ac.

[mo271]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style