Proof of extend_perm_over_itcomp