Proof of equiv_rel_self_functionality