This is an implementation of the Falso (TM) HyperProver (TM), written in the process of learning Lean. I do not guarantee it is in any way as performant as other implementations of Falso (TM), or, indeed as powerful.
But it sure makes proving stuff much easier.