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?