Moving equality across an implication

[David Starner]

I'm have trouble with this, and I can't find an example in the set.mm.
How would you prove something like zeroimpxpxeqzero $p |- ( x = 0 -> x
+ x = 0 ) ? (or x = 1 -> x + x = 2, etc.) I've got a similar problem
in group theory that would be trivial if I could find something to
move the equality across the implication and convert it into 0 + 0 =
0.

--
The standard is written in English . If you have trouble understanding
a particular section, read it again and again and again . . . Sit up
straight. Eat your vegetables. Do not mumble. -- _Pascal_, ISO 7185
(1991)

[Alexander van der Vekens]

Hi David,

I think the theorem should be zeroimpxpxeqzero $p |- ( x = 0 -> ( x
+ x ) = 0 ) (with brackets).

then you can use eqtrd and oveq12d to replace x by 0, resulting in ( x = 0 -> ( 0
+ 0 ) = 0 ). Then apply a1i and 00id.

Alexander