Consider the following premises. forall x: T_2(x). t <-> w_1. ~w_1. Can we infer T_2(a_11) from them? If possible, name the inference rules being used at each step.
 From t <-> w_1, ~w_1 we can infer ~t via biconditional elimination. Finally, from forall x: T_2(x) we can infer T_2(a_11) via universal instantiation. Therefore, the answer is yes.