Consider the following premises. forall y: ~U_2(y). p_1. t <-> U_2(e). Can we infer ~t from them?
 From forall y: ~U_2(y) we can infer ~U_2(e). Finally, from t <-> U_2(e), ~U_2(e) we can infer ~t. Therefore, the answer is yes.