Explicit free magmas

Stream: Equational

[Amir Livne Bar-on]

After the discussion a few days ago, I decided to try to prove an explicit form for the free magmas with some laws.

My first attempt was at one of the simplest magmas, for the associative law. The code is at equational#807.

It took a while to make, which would be expected as this is my first serious formalization, but I'm also surprised by how long the code is. Maybe it's because I chose to use List rather than defining a new inductive type for NonEmptyList? If anyone with more experience can look at the code I'd appreciate it.

[Alex Meiburg]

I looked at it. I'm by no means a Lean pro, but it looks like a reasonable length for what you're doing. DeBrujin factors are brutal!