Consider the following premises. forall x_9: R_9(x_9) <-> S_9(x_9). S_9(h) -> R_9(h). Can we infer R_9(h) -> S_9(h) from them?
 From forall x_9: R_9(x_9) <-> S_9(x_9) we can infer R_9(h) <-> S_9(h). Finally, from R_9(h) <-> S_9(h) we can infer R_9(h) -> S_9(h). Therefore, the answer is yes.