That's a different style of proof, based on equational reasoning; Agda [0], Coq [1] and Lean [2] are three theorem provers that work with those proofs better. B

That's a different style of proof, based on equational reasoning; Agda [0], Coq [1] and Lean [2] are three theorem provers that work with those proofs better. Being able to quickly and informally perform equational reasoning on functional programs is also what (imo) makes those languages easier to think about, so it's a valuable skill outside of proving. [0]: https://wiki.portal.chalmers.se/agda/pmwiki.php https://wiki.portal.chalmers.se/agda/pmwiki.php [1]: https://coq.inria.fr/ https://coq.inria.fr/ [2]: https://leanprover.github.io/ https://leanprover.github.io/