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