Consider the following premises. forall x_16: P_16(x_16) <-> Q(x_16). forall x_16: P_16(x_16). Can we infer ~Q(g) from them?
 From forall x_16: P_16(x_16) <-> Q(x_16) we can infer forall x_16: P_16(x_16) -> Q(x_16). Finally, from forall x_16: P_16(x_16) -> Q(x_16), forall x_16: P_16(x_16) we can infer forall x_16: Q(x_16), which contradicts ~Q(g). Therefore, the answer is no.