Proof of squash_functionality_wrt_implies