Proof of refl_functionality_wrt_iff