validation of an inference rule using a proof assistant

[bhpayne]

The inference rule "add x to both sides of an expression" is used in many different derivations, but the proof of that inference rule only needs to be implemented once.

Building on what's already available from Mizar or Metamath would be cool, although I could also understand building a proof from scratch. I'm not clear which of those options requires more or less work.

There are many proof assistance available; see https://en.wikipedia.org/wiki/Proof_assistant#Comparison_of_systems Which gets used is not important. Nor is the logical basis.

Selecting a sufficiently capable logical basis and then seeing whether a few of the simple inference rules can be given a solid foundation would be useful.