Proof of xxrefl_functionality_wrt_breqv