How to solve Hoare's problem when precondition contains meta symbols?

This is the proram for which I have to prove correctness using Hoare's Axioms:

{X = |x|}

if(x<=0)

x:=-x;

else

skip;

{X=x}


This is my solution so far by applying Haore's conditional transformation:

(x<=0 => wp(x:=-x; X=x)) ^ (~(x<=0) => wp(skip, X=x))

(x<=0 => X=-x) ^ (~(x<=0) => X=x)


Now the thing I am confused about is how can I prove X = |x|?