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