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