How to prove (X !-> 3) =[ <{ X := X + 2 }> ]=> (X !-> 5)?

Question

I know how to prove 3 + 2 = 5 using Imp, defined in Software Foundations, Volume 1.

Definition plus2_3_is_5: Prop := forall (st: state),
  (X !-> 3) =[ <{ X := X + 2 }> ]=> st -> st X = 5.

Fact plus2_3_is_5_fact : plus2_3_is_5.
Proof.
  intros st H.
  inversion H. subst. simpl.
  apply t_update_eq. (* or use [reflexivity] *)
Qed.

But when I define plus2_3_is_5 to be (X !-> 3) =[ <{ X := X + 2 }> ]=> (X !-> 5), I couldn't find the proof. Can anyone help on this?

When I use the proposition

forall (st: state),
  (X !-> 3) =[ <{ X := X + 2 }> ]=> st -> st X = 5.

to express 3 + 2 = 5, I could get the proof correctly. But when I use the apparently simpler proposition

(X !-> 3) =[ <{ X := X + 2 }> ]=> (X !-> 5)

instead, every tactic I tried, such as apply E_Asgn, apply t_update_eq, failed.

Answer 1

I got the solution with the help of ayylien.

Fact plus2_3_is_5_fact :
  (X !-> 3) =[ <{ X := X + 2 }> ]=> (X !-> 5).
Proof.
  assert (H: (X !-> 5; X !-> 3) = (X !-> 5)).
  { apply t_update_shadow. }
  rewrite <- H. 
  apply E_Asgn. reflexivity.
Qed.