Consider the following premises. t -> U(a_10). U_4(a_10) -> t. forall z: U(z) -> U_4(z). Can we infer ~(t <-> U(a_10)) from them? If possible, name the inference rules being used at each step.
 From forall z: U(z) -> U_4(z) we can infer U(a_10) -> U_4(a_10) via universal instantiation. From U(a_10) -> U_4(a_10), U_4(a_10) -> t we can infer U(a_10) -> t via transitivity. Finally, from t -> U(a_10), U(a_10) -> t we can infer t <-> U(a_10) via biconditional introduction, which contradicts ~(t <-> U(a_10)). Therefore, the answer is no.