Hey PK, this is great! Your idea to use a proofGrid
function to visualize which axioms are redundant to the proofs of particular theorems is one of the most innovative pieces of metamathematics that I've seen anyone attempt using FindEquationalProof
! Kudos!