Sorry if an improper question, looking into metamath and metamath-lamp and though it should be trivial to prove A = 2 -> ( A + 2 ) = 4, or the inverse. But cant seem to get it right in metamath-lamp. Starting with hypothesis H ( A + 2 ) = 4 it should (?) be possible, even simple, to get to: G A = 2 Started with: - H |- ( A + 2 ) = 4 - P 2p2e4 |- ( 2 + 2 ) = 4 - P eqtr4i |- ( A + 2 ) = ( 2 + 2 ) After this, I'm blocked, cant find the steps that get to the goal: A = 2 Wouldn't some existing simplification do the trick? Does it exists in set.mm? How do I apply it?