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