Equational reasoning meets Induction (part 1)

I’ve been studying Formal Methods again since the beggining of this year, and now I’m looking at algebraic specifications and I found they pretty elegant. To be able to pratice with it I vibecoded an algebraic specification plugin for Claude, and named it algae . Since I more interested into understanding the proofs I’m focusing on a syntax that make everything explicit, instead of focusing on soundness and the checker now. I came across Algebraic Specifications while going through this book: At chapter 13