Consider the following premises. S_12(f_2) -> s_1. s_1 -> R_12(f_2). forall x_12: R_12(x_12) <-> S_12(x_12). Can we infer s_1 <-> R_12(f_2) from them?
 From forall x_12: R_12(x_12) <-> S_12(x_12) we can infer R_12(f_2) <-> S_12(f_2). From R_12(f_2) <-> S_12(f_2) we can infer R_12(f_2) -> S_12(f_2). From R_12(f_2) -> S_12(f_2), S_12(f_2) -> s_1 we can infer R_12(f_2) -> s_1. Finally, from s_1 -> R_12(f_2), R_12(f_2) -> s_1 we can infer s_1 <-> R_12(f_2). Therefore, the answer is yes.