Visible dependent quantification / CUSKs