Consider the following premises. forall z: ~W_4(z). w_1. W_4(g) <-> t_1. Can we infer ~t_1 and w_1 from them?
 From forall z: ~W_4(z) we can infer ~W_4(g). From W_4(g) <-> t_1, ~W_4(g) we can infer ~t_1. Finally, from ~t_1, w_1 we can infer ~t_1 and w_1. Therefore, the answer is yes.