Suppose I have those hypothesis:

`ForAll[a , sin[2a]== 2 sin[a]*cos[a]]`

and

`sin[2* x]==1`

I want to apply the property 1) to the equation 2) and obtain:

3)`2sin[x]*cos[x]== 1`

I know I can achieve it with a pattern matching: sin[2 x] == 1/.sin [2 a_] :> 2sin [a]cos[a] but I want to do it with a ForAll!!