Proof of binrel_eqv_functionality_wrt_breqv