Consider the following premises. forall y_4: ~S_1(y_4). S_7(a_7) <-> S_1(a). forall x_7: W(x_7) <-> S_7(x_7). Can we infer ~W(a_7) from them? If possible, name the inference rules being used at each step.
 From forall y_4: ~S_1(y_4) we can infer ~S_1(a) via universal instantiation. From forall x_7: W(x_7) <-> S_7(x_7) we can infer W(a_7) <-> S_7(a_7) via universal instantiation. From S_7(a_7) <-> S_1(a), ~S_1(a) we can infer ~S_7(a_7) via biconditional elimination. Finally, from W(a_7) <-> S_7(a_7), ~S_7(a_7) we can infer ~W(a_7) via biconditional elimination. Therefore, the answer is yes.