{
    [a]
    {
        P(a)
        ___
        E y . P(y)
    }
    P(a) -> E y . P(y)
}

A y . P(y) -> E y . P(y)