{1}   1 forall x(Vx implies Px)                      P
{2}   2 forall x[forall y(Ex & Py implies not Lxy)]  P
{1}   3 Vb implies Pb                                US
{2}   4 Ea & Pb implies not Lab                      US
{2}   5 Ea & Lab implies not Pb                      4 T
{1}   6 not Pb imlies not Vb                         3 T
{1,2} 7 Ea & Vb implies not Lab                      3&4 T
{1,2} 8 forall x[forall y(Ex & Vy implies not Lxy)]  UG