lthms ⸮ is a user on mastodon.social. You can follow them or interact with them if you have an account anywhere in the fediverse.
If you don't, you can sign up here.
Proofs written with the #Coq equations plugins are really interesting, because you end up using `rewrite` all the time.
