Proof of restrict_perm_using_txpose