Proof of not_functionality_wrt_implies