The Leibniz rule is probably the single most important one for mathematically sound programming. He was a real dreamer. It’s odd how hard it is to search for,

The Leibniz rule is probably the single most important one for mathematically sound programming. He was a real dreamer. It’s odd how hard it is to search for, but one formulation is x=y => f.x=f.y In this case the dot is the function application operator. Note that this is a logical or syntactic rule and not an operational one. It’s saying that you can freely substitute, for all f, with renaming, the function body of f in equations of x and y.