Consider the following premises. S_2(a_1) -> S_4(a_1). forall y_3: S_2(y_3) <-> S_4(y_3). Can we infer S_2(a_1) <-> S_4(a_1) from them? If possible, name the inference rules being used at each step.
We can infer S_2(a_1) <-> S_4(a_1) via the universal instantiation rule. Therefore, the answer is yes.