very cool. btw, I also love that "sorry" is the "any" equivalent in Lean