https://github.com/Experiential-Reality/theory/tree/main/lean/BLD/Lie I've been working on using lean to proof my ideas, this fell out. Is it useful beyond just me? Should I make a pull request?