Proof of extend_restrict_perm_cancel