Proof of extend_perm_over_comp