Sorry if a 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 a simplification with ( X F A ) = ( Y F A ) -> X = Y do the trick? Does it exists in set.mm? How do I apply it?

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?