This adds a confluence proof for 3588 !-> ..., which is interesting
since it is turned by Vampire and kbcv into a system of two confluent
rules, which are then implemented using Joachim Breitner's Confluence
system (with some enhancements).

Not sure if it should be merged as is because it is quite slow to
compile, due to the massive automated case splitting through the custom
"sledgehammer" tactic that it employs (it's somewhat fine to have it
alone, but if 10-100 more like this would probably be a problem).

Perhaps someone who is more experienced at Lean elaboration performance
optimization can find a way to speed it up (and also automate it more
ideally); otherwise it's possible that some other strategy for making
confluence proofs needs to be found, or possibly a build system change
where some proofs are not compiled by default.

EDIT: I rewrote the proof and now it's fast and good and all these
problems are solved